𝕜 : Type u_2
E : Type u_1
F : Type ?u.55065
ι : Type ?u.55068
π : ι → Type ?u.55073
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x✝ x : E
hx : x ∈ extremePoints 𝕜 (↑(convexHull 𝕜).toOrderHom A)
⊢ x ∈ A
𝕜 : Type u_2
E : Type u_1
F : Type ?u.55065
ι : Type ?u.55068
π : ι → Type ?u.55073
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
⊢ extremePoints 𝕜 (↑(convexHull 𝕜).toOrderHom A) ⊆ A
rintro x hx
𝕜 : Type u_2
E : Type u_1
F : Type ?u.55065
ι : Type ?u.55068
π : ι → Type ?u.55073
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x✝ x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom A ∧ Convex 𝕜 (↑(convexHull 𝕜).toOrderHom A \ {x})
⊢ x ∈ A
𝕜 : Type u_2
E : Type u_1
F : Type ?u.55065
ι : Type ?u.55068
π : ι → Type ?u.55073
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x✝ x : E
hx : x ∈ extremePoints 𝕜 (↑(convexHull 𝕜).toOrderHom A)
⊢ x ∈ A
rw [(convex_convexHull 𝕜 _).mem_extremePoints_iff_convex_diff] at hx
𝕜 : Type u_2
E : Type u_1
F : Type ?u.55065
ι : Type ?u.55068
π : ι → Type ?u.55073
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x✝ x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom A ∧ Convex 𝕜 (↑(convexHull 𝕜).toOrderHom A \ {x})
h : ¬x ∈ A
⊢ False
𝕜 : Type u_2
E : Type u_1
F : Type ?u.55065
ι : Type ?u.55068
π : ι → Type ?u.55073
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x✝ x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom A ∧ Convex 𝕜 (↑(convexHull 𝕜).toOrderHom A \ {x})
⊢ x ∈ A
by_contra h
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.55065
ι : Type ?u.55068
π : ι → Type ?u.55073
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x✝ x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom A ∧ Convex 𝕜 (↑(convexHull 𝕜).toOrderHom A \ {x})
h : ¬x ∈ A
⊢ False
exact (convexHull_min (subset_diff.2 ⟨subset_convexHull 𝕜 _, disjoint_singleton_right.2 h⟩) hx.2
  hx.1).2 rfl