𝕜 : Type u_2
E : Type u_1
F : Type ?u.5166
ι : Type ?u.5169
π : ι → Type ?u.5174
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x : E
⊢ x ∈ extremePoints 𝕜 A → IsExtreme 𝕜 A {x}
𝕜 : Type u_2
E : Type u_1
F : Type ?u.5166
ι : Type ?u.5169
π : ι → Type ?u.5174
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x : E
⊢ x ∈ extremePoints 𝕜 A ↔ IsExtreme 𝕜 A {x}
refine' ⟨_, fun hx ↦ ⟨singleton_subset_iff.1 hx.1, fun x₁ hx₁ x₂ hx₂ ↦ hx.2 hx₁ hx₂ rfl⟩⟩
case intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.5166
ι : Type ?u.5169
π : ι → Type ?u.5174
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x : E
hxA : x ∈ A
hAx : ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
⊢ IsExtreme 𝕜 A {x}
𝕜 : Type u_2
E : Type u_1
F : Type ?u.5166
ι : Type ?u.5169
π : ι → Type ?u.5174
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x : E
⊢ x ∈ extremePoints 𝕜 A → IsExtreme 𝕜 A {x}
rintro ⟨hxA, hAx⟩
case intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.5166
ι : Type ?u.5169
π : ι → Type ?u.5174
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x : E
hxA : x ∈ A
hAx : ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
⊢ ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → ∀ ⦃x_1 : E⦄, x_1 ∈ {x} → x_1 ∈ openSegment 𝕜 x₁ x₂ → x₁ ∈ {x} ∧ x₂ ∈ {x}
case intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.5166
ι : Type ?u.5169
π : ι → Type ?u.5174
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x : E
hxA : x ∈ A
hAx : ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
⊢ IsExtreme 𝕜 A {x}
use singleton_subset_iff.2 hxA
case intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.5166
ι : Type ?u.5169
π : ι → Type ?u.5174
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
y : E
hxA : y ∈ A
hAx : ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → y ∈ openSegment 𝕜 x₁ x₂ → x₁ = y ∧ x₂ = y
⊢ y ∈ openSegment 𝕜 x₁ x₂ → x₁ ∈ {y} ∧ x₂ ∈ {y}
case intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.5166
ι : Type ?u.5169
π : ι → Type ?u.5174
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x : E
hxA : x ∈ A
hAx : ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
⊢ ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → ∀ ⦃x_1 : E⦄, x_1 ∈ {x} → x_1 ∈ openSegment 𝕜 x₁ x₂ → x₁ ∈ {x} ∧ x₂ ∈ {x}
rintro x₁ hx₁A x₂ hx₂A y (rfl : y = x)
no goals
case intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.5166
ι : Type ?u.5169
π : ι → Type ?u.5174
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
y : E
hxA : y ∈ A
hAx : ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → y ∈ openSegment 𝕜 x₁ x₂ → x₁ = y ∧ x₂ = y
⊢ y ∈ openSegment 𝕜 x₁ x₂ → x₁ ∈ {y} ∧ x₂ ∈ {y}
exact hAx hx₁A hx₂A