𝕜 : Type u_1
E : Type u_2
F : Type ?u.45230
ι : Type ?u.45233
π : ι → Type ?u.45238
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hA : Convex 𝕜 A
⊢ x ∈ A ∧ Convex 𝕜 (A \ {x}) → x ∈ extremePoints 𝕜 A
𝕜 : Type u_1
E : Type u_2
F : Type ?u.45230
ι : Type ?u.45233
π : ι → Type ?u.45238
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hA : Convex 𝕜 A
⊢ x ∈ extremePoints 𝕜 A ↔ x ∈ A ∧ Convex 𝕜 (A \ {x})
use fun hx ↦ ⟨hx.1, (mem_extremePoints_iff_extreme_singleton.1 hx).convex_diff hA⟩
case intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.45230
ι : Type ?u.45233
π : ι → Type ?u.45238
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : Convex 𝕜 (A \ {x})
⊢ x ∈ extremePoints 𝕜 A
𝕜 : Type u_1
E : Type u_2
F : Type ?u.45230
ι : Type ?u.45233
π : ι → Type ?u.45238
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hA : Convex 𝕜 A
⊢ x ∈ A ∧ Convex 𝕜 (A \ {x}) → x ∈ extremePoints 𝕜 A
rintro ⟨hxA, hAx⟩
case intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.45230
ι : Type ?u.45233
π : ι → Type ?u.45238
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : Convex 𝕜 (A \ {x})
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx : x ∈ [x₁-[𝕜]x₂]
⊢ x₁ = x ∨ x₂ = x
case intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.45230
ι : Type ?u.45233
π : ι → Type ?u.45238
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : Convex 𝕜 (A \ {x})
⊢ x ∈ extremePoints 𝕜 A
refine' mem_extremePoints_iff_forall_segment.2 ⟨hxA, fun x₁ hx₁ x₂ hx₂ hx ↦ _⟩
case intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.45230
ι : Type ?u.45233
π : ι → Type ?u.45238
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : ∀ ⦃x_1 : E⦄, x_1 ∈ A \ {x} → ∀ ⦃y : E⦄, y ∈ A \ {x} → [x_1-[𝕜]y] ⊆ A \ {x}
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx : x ∈ [x₁-[𝕜]x₂]
⊢ x₁ = x ∨ x₂ = x
case intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.45230
ι : Type ?u.45233
π : ι → Type ?u.45238
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : Convex 𝕜 (A \ {x})
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx : x ∈ [x₁-[𝕜]x₂]
⊢ x₁ = x ∨ x₂ = x
rw [convex_iff_segment_subset] at hAx
case intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.45230
ι : Type ?u.45233
π : ι → Type ?u.45238
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : ∀ ⦃x_1 : E⦄, x_1 ∈ A \ {x} → ∀ ⦃y : E⦄, y ∈ A \ {x} → [x_1-[𝕜]y] ⊆ A \ {x}
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx : x ∈ [x₁-[𝕜]x₂]
h : x₁ ≠ x ∧ x₂ ≠ x
⊢ False
case intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.45230
ι : Type ?u.45233
π : ι → Type ?u.45238
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : ∀ ⦃x_1 : E⦄, x_1 ∈ A \ {x} → ∀ ⦃y : E⦄, y ∈ A \ {x} → [x_1-[𝕜]y] ⊆ A \ {x}
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx : x ∈ [x₁-[𝕜]x₂]
⊢ x₁ = x ∨ x₂ = x
by_contra' h
no goals
case intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.45230
ι : Type ?u.45233
π : ι → Type ?u.45238
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : ∀ ⦃x_1 : E⦄, x_1 ∈ A \ {x} → ∀ ⦃y : E⦄, y ∈ A \ {x} → [x_1-[𝕜]y] ⊆ A \ {x}
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx : x ∈ [x₁-[𝕜]x₂]
h : x₁ ≠ x ∧ x₂ ≠ x
⊢ False
exact (hAx ⟨hx₁, fun hx₁ ↦ h.1 (mem_singleton_iff.2 hx₁)⟩
    ⟨hx₂, fun hx₂ ↦ h.2 (mem_singleton_iff.2 hx₂)⟩ hx).2 rfl