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

State before:
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
⊢ BddBelow (f '' s)
Tactic:
cases s.eq_empty_or_nonempty with
| inl h =>
    simp only [h, Set.image_empty]
    exact bddBelow_empty
| inr h =>
    obtain ⟨a, _, has⟩ := LowerSemicontinuousOn.exists_forall_le_of_isCompact h hs hf
    use f a
    rintro b ⟨x, hx, rfl⟩; exact has x hx
State after:
no goals

State before:
case inl
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : s = ∅
⊢ BddBelow (f '' s)
Tactic:
simp only [h, Set.image_empty]
State after:
case inl
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : s = ∅
⊢ BddBelow ∅

State before:
case inl
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : s = ∅
⊢ BddBelow ∅
Tactic:
exact bddBelow_empty
State after:
no goals

State before:
case inr
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Set.Nonempty s
⊢ BddBelow (f '' s)
Tactic:
obtain ⟨a, _, has⟩ := LowerSemicontinuousOn.exists_forall_le_of_isCompact h hs hf
State after:
case inr.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Set.Nonempty s
a : α
left✝ : a ∈ s
has : ∀ x ∈ s, f a ≤ f x
⊢ BddBelow (f '' s)

State before:
case inr.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Set.Nonempty s
a : α
left✝ : a ∈ s
has : ∀ x ∈ s, f a ≤ f x
⊢ BddBelow (f '' s)
Tactic:
use f a
State after:
case h
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Set.Nonempty s
a : α
left✝ : a ∈ s
has : ∀ x ∈ s, f a ≤ f x
⊢ f a ∈ lowerBounds (f '' s)

State before:
case h
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Set.Nonempty s
a : α
left✝ : a ∈ s
has : ∀ x ∈ s, f a ≤ f x
⊢ f a ∈ lowerBounds (f '' s)
Tactic:
rintro b ⟨x, hx, rfl⟩
State after:
case h.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Set.Nonempty s
a : α
left✝ : a ∈ s
has : ∀ x ∈ s, f a ≤ f x
x : α
hx : x ∈ s
⊢ f a ≤ f x

State before:
case h.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Set.Nonempty s
a : α
left✝ : a ∈ s
has : ∀ x ∈ s, f a ≤ f x
x : α
hx : x ∈ s
⊢ f a ≤ f x
Tactic:
exact has x hx
State after:
no goals