case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : E →L[𝕜] 𝕜
A✝ B C : Set E
X : Finset E
x : E
inst✝ : OrderClosedTopology 𝕜
A : Set E
hA : IsClosed A
hAB : IsExposed 𝕜 A ∅
⊢ IsClosed ∅

case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : E →L[𝕜] 𝕜
A✝ B✝ C : Set E
X : Finset E
x : E
inst✝ : OrderClosedTopology 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
hA : IsClosed A
hB : Set.Nonempty B
⊢ IsClosed B
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : E →L[𝕜] 𝕜
A✝ B✝ C : Set E
X : Finset E
x : E
inst✝ : OrderClosedTopology 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
hA : IsClosed A
⊢ IsClosed B
obtain rfl | hB := B.eq_empty_or_nonempty
case inr.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l✝ : E →L[𝕜] 𝕜
A✝ B C : Set E
X : Finset E
x : E
inst✝ : OrderClosedTopology 𝕜
A : Set E
hA : IsClosed A
l : E →L[𝕜] 𝕜
a : 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ a ≤ ↑l x}
hB : Set.Nonempty {x | x ∈ A ∧ a ≤ ↑l x}
⊢ IsClosed {x | x ∈ A ∧ a ≤ ↑l x}
case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : E →L[𝕜] 𝕜
A✝ B✝ C : Set E
X : Finset E
x : E
inst✝ : OrderClosedTopology 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
hA : IsClosed A
hB : Set.Nonempty B
⊢ IsClosed B
obtain ⟨l, a, rfl⟩ := hAB.eq_inter_halfspace' hB
no goals
case inr.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l✝ : E →L[𝕜] 𝕜
A✝ B C : Set E
X : Finset E
x : E
inst✝ : OrderClosedTopology 𝕜
A : Set E
hA : IsClosed A
l : E →L[𝕜] 𝕜
a : 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ a ≤ ↑l x}
hB : Set.Nonempty {x | x ∈ A ∧ a ≤ ↑l x}
⊢ IsClosed {x | x ∈ A ∧ a ≤ ↑l x}
exact hA.isClosed_le continuousOn_const l.continuous.continuousOn
no goals
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : E →L[𝕜] 𝕜
A✝ B C : Set E
X : Finset E
x : E
inst✝ : OrderClosedTopology 𝕜
A : Set E
hA : IsClosed A
hAB : IsExposed 𝕜 A ∅
⊢ IsClosed ∅
simp