Theorems · Theorem · general topology

LowerSemicontinuousOn.isCompact_inter_preimage_Iic

∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_4} [inst_1 : LinearOrder γ] {f : α → γ},
  LowerSemicontinuousOn f s → IsCompact s → ∀ (c : γ), IsCompact (s ∩ f ⁻¹' Set.Iic c)

The sublevel sets of a lower semicontinuous function on a compact set are compact.

Defined in

Mathlib.Topology.Semicontinuity.Basic

Cited by

2 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceLinearOrder