Theorem: LowerSemicontinuousOn.exists_iInf_of_isCompact (Sion/Semicontinuous.lean)

State before:
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
⊢ ∃ a ∈ s, f a = ⨅ x ∈ s, f x
Tactic:
obtain ⟨a, ha, ha_le⟩ := LowerSemicontinuousOn.exists_forall_le_of_isCompact ne_s hs hf
State after:
case intro.intro
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ ∃ a ∈ s, f a = ⨅ x ∈ s, f x

State before:
case intro.intro
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ ∃ a ∈ s, f a = ⨅ x ∈ s, f x
Tactic:
use a
State after:
case h
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ a ∈ s ∧ f a = ⨅ x ∈ s, f x

State before:
case h
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ a ∈ s ∧ f a = ⨅ x ∈ s, f x
Tactic:
apply And.intro ha
State after:
case h
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ f a = ⨅ x ∈ s, f x

State before:
case h
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ f a = ⨅ x ∈ s, f x
Tactic:
apply le_antisymm
State after:
case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ f a ≤ ⨅ x ∈ s, f x

case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ ⨅ x ∈ s, f x ≤ f a

State before:
case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ f a ≤ ⨅ x ∈ s, f x

case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ ⨅ x ∈ s, f x ≤ f a
Tactic:
rw [le_iInf₂_iff]
State after:
case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ ∀ i ∈ s, f a ≤ f i

case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ ⨅ x ∈ s, f x ≤ f a

State before:
case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ ∀ i ∈ s, f a ≤ f i

case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ ⨅ x ∈ s, f x ≤ f a
Tactic:
intro x hx
State after:
case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
x : α
hx : x ∈ s
⊢ f a ≤ f x

case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ ⨅ x ∈ s, f x ≤ f a

State before:
case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
x : α
hx : x ∈ s
⊢ f a ≤ f x

case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ ⨅ x ∈ s, f x ≤ f a
Tactic:
exact ha_le x hx
State after:
case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ ⨅ x ∈ s, f x ≤ f a

State before:
case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ ⨅ x ∈ s, f x ≤ f a
Tactic:
exact iInf₂_le a ha
State after:
no goals