𝕜 : Type u_1
E : Type u_2
F : Type ?u.2321
ι : Type ?u.2324
π : ι → Type ?u.2329
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x : E
hAB : IsExtreme 𝕜 A B
hAC : IsExtreme 𝕜 A C
⊢ ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → ∀ ⦃x : E⦄, x ∈ B ∩ C → x ∈ openSegment 𝕜 x₁ x₂ → x₁ ∈ B ∩ C ∧ x₂ ∈ B ∩ C
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2321
ι : Type ?u.2324
π : ι → Type ?u.2329
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x : E
hAB : IsExtreme 𝕜 A B
hAC : IsExtreme 𝕜 A C
⊢ IsExtreme 𝕜 A (B ∩ C)
use Subset.trans (inter_subset_left _ _) hAB.1
case intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2321
ι : Type ?u.2324
π : ι → Type ?u.2329
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x✝ : E
hAB : IsExtreme 𝕜 A B
hAC : IsExtreme 𝕜 A C
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxB : x ∈ B
hxC : x ∈ C
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ B ∩ C ∧ x₂ ∈ B ∩ C
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2321
ι : Type ?u.2324
π : ι → Type ?u.2329
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x : E
hAB : IsExtreme 𝕜 A B
hAC : IsExtreme 𝕜 A C
⊢ ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → ∀ ⦃x : E⦄, x ∈ B ∩ C → x ∈ openSegment 𝕜 x₁ x₂ → x₁ ∈ B ∩ C ∧ x₂ ∈ B ∩ C
rintro x₁ hx₁A x₂ hx₂A x ⟨hxB, hxC⟩ hx
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2321
ι : Type ?u.2324
π : ι → Type ?u.2329
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x✝ : E
hAB : IsExtreme 𝕜 A B
hAC : IsExtreme 𝕜 A C
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxB : x ∈ B
hxC : x ∈ C
hx : x ∈ openSegment 𝕜 x₁ x₂
hx₁B : x₁ ∈ B
hx₂B : x₂ ∈ B
⊢ x₁ ∈ B ∩ C ∧ x₂ ∈ B ∩ C
case intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2321
ι : Type ?u.2324
π : ι → Type ?u.2329
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x✝ : E
hAB : IsExtreme 𝕜 A B
hAC : IsExtreme 𝕜 A C
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxB : x ∈ B
hxC : x ∈ C
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ B ∩ C ∧ x₂ ∈ B ∩ C
obtain ⟨hx₁B, hx₂B⟩ := hAB.2 hx₁A hx₂A hxB hx
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2321
ι : Type ?u.2324
π : ι → Type ?u.2329
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x✝ : E
hAB : IsExtreme 𝕜 A B
hAC : IsExtreme 𝕜 A C
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxB : x ∈ B
hxC : x ∈ C
hx : x ∈ openSegment 𝕜 x₁ x₂
hx₁B : x₁ ∈ B
hx₂B : x₂ ∈ B
hx₁C : x₁ ∈ C
hx₂C : x₂ ∈ C
⊢ x₁ ∈ B ∩ C ∧ x₂ ∈ B ∩ C
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2321
ι : Type ?u.2324
π : ι → Type ?u.2329
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x✝ : E
hAB : IsExtreme 𝕜 A B
hAC : IsExtreme 𝕜 A C
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxB : x ∈ B
hxC : x ∈ C
hx : x ∈ openSegment 𝕜 x₁ x₂
hx₁B : x₁ ∈ B
hx₂B : x₂ ∈ B
⊢ x₁ ∈ B ∩ C ∧ x₂ ∈ B ∩ C
obtain ⟨hx₁C, hx₂C⟩ := hAC.2 hx₁A hx₂A hxC hx
no goals
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2321
ι : Type ?u.2324
π : ι → Type ?u.2329
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x✝ : E
hAB : IsExtreme 𝕜 A B
hAC : IsExtreme 𝕜 A C
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxB : x ∈ B
hxC : x ∈ C
hx : x ∈ openSegment 𝕜 x₁ x₂
hx₁B : x₁ ∈ B
hx₂B : x₂ ∈ B
hx₁C : x₁ ∈ C
hx₂C : x₂ ∈ C
⊢ x₁ ∈ B ∩ C ∧ x₂ ∈ B ∩ C
exact ⟨⟨hx₁B, hx₁C⟩, hx₂B, hx₂C⟩