inter — Mathlib

English

If B and C are extreme in A, then their intersection B ∩ C is extreme in A.

Русский

Если B и C являются крайними внутри A, то их пересечение B ∩ C также крайно в A.

LaTeX

$$$\text{If } IsExtreme 𝕜 A B \text{ and } IsExtreme 𝕜 A C, \text{ then } IsExtreme 𝕜 A (B \cap C).$$$

Lean4

theorem inter (hAB : IsExtreme 𝕜 A B) (hAC : IsExtreme 𝕜 A C) : IsExtreme 𝕜 A (B ∩ C) :=
  by
  use Subset.trans inter_subset_left hAB.1
  rintro x₁ hx₁A x₂ hx₂A x ⟨hxB, hxC⟩ hx
  exact ⟨hAB.left_mem_of_mem_openSegment hx₁A hx₂A hxB hx, hAC.left_mem_of_mem_openSegment hx₁A hx₂A hxC hx⟩

Похожие утверждения