𝕜 : 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
hAB : IsExposed 𝕜 A B
x : E
hx : x ∈ B
⊢ x ∈ A
𝕜 : 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
hAB : IsExposed 𝕜 A B
⊢ B ⊆ A
rintro x hx
case 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 C : Set E
X : Finset E
x✝ x : E
w✝ : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑w✝ y ≤ ↑w✝ x}
hx : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑w✝ y ≤ ↑w✝ x}
⊢ x ∈ A
𝕜 : 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
hAB : IsExposed 𝕜 A B
x : E
hx : x ∈ B
⊢ x ∈ A
obtain ⟨_, rfl⟩ := hAB ⟨x, hx⟩
no goals
case 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 C : Set E
X : Finset E
x✝ x : E
w✝ : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑w✝ y ≤ ↑w✝ x}
hx : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑w✝ y ≤ ↑w✝ x}
⊢ x ∈ A
exact hx.1