Theorem: UpperSemicontinuousOn.exists_forall_ge_of_isCompact (Sion/Semicontinuous.lean)

State before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : UpperSemicontinuousOn f s
⊢ ∃ a ∈ s, ∀ x ∈ s, f x ≤ f a
Tactic:
apply LowerSemicontinuousOn.exists_forall_le_of_isCompact (β := βᵒᵈ) ne_s hs
State after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : UpperSemicontinuousOn f s
⊢ LowerSemicontinuousOn (fun x => f x) s

State before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : UpperSemicontinuousOn f s
⊢ LowerSemicontinuousOn (fun x => f x) s
Tactic:
exact hf
State after:
no goals