𝕜 : Type u_1
E : Type u_2
F : Type ?u.1093
ι : Type ?u.1096
π : ι → Type ?u.1101
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x✝ : E
hAB : IsExtreme 𝕜 A B
hBC : IsExtreme 𝕜 B C
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxC : x ∈ C
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ C ∧ x₂ ∈ C
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1093
ι : Type ?u.1096
π : ι → Type ?u.1101
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x : E
hAB : IsExtreme 𝕜 A B
hBC : IsExtreme 𝕜 B C
⊢ IsExtreme 𝕜 A C
refine' ⟨Subset.trans hBC.1 hAB.1, fun x₁ hx₁A x₂ hx₂A x hxC hx ↦ _⟩
case intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1093
ι : Type ?u.1096
π : ι → Type ?u.1101
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x✝ : E
hAB : IsExtreme 𝕜 A B
hBC : IsExtreme 𝕜 B C
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxC : x ∈ C
hx : x ∈ openSegment 𝕜 x₁ x₂
hx₁B : x₁ ∈ B
hx₂B : x₂ ∈ B
⊢ x₁ ∈ C ∧ x₂ ∈ C
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1093
ι : Type ?u.1096
π : ι → Type ?u.1101
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x✝ : E
hAB : IsExtreme 𝕜 A B
hBC : IsExtreme 𝕜 B C
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxC : x ∈ C
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ C ∧ x₂ ∈ C
obtain ⟨hx₁B, hx₂B⟩ := hAB.2 hx₁A hx₂A (hBC.1 hxC) hx
no goals
case intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1093
ι : Type ?u.1096
π : ι → Type ?u.1101
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x✝ : E
hAB : IsExtreme 𝕜 A B
hBC : IsExtreme 𝕜 B C
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxC : x ∈ C
hx : x ∈ openSegment 𝕜 x₁ x₂
hx₁B : x₁ ∈ B
hx₂B : x₂ ∈ B
⊢ x₁ ∈ C ∧ x₂ ∈ C
exact hBC.2 hx₁B hx₂B hxC hx