Theorems · Theorem · general topology

LowerSemicontinuousOn.exists_isMinOn

∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → β} [inst_1 : LinearOrder β] {s : Set α},
  s.Nonempty → IsCompact s → LowerSemicontinuousOn f s → ∃ a ∈ s, IsMinOn f s a

A lower semicontinuous function attains its lower bound on a nonempty compact set.

Defined in

Mathlib.Topology.Semicontinuity.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrder