mem_closedInterior_iff_wbtw — Mathlib

English

The closed interior of a 1-dimensional face of a simplex is the segment joining its two vertex points.

Русский

У замкнутой внутренности грани 1-мерного симплекса есть место между двумя её вершинами, и это отрезок между ними.

LaTeX

$$(s.face (Finset.card_pair h)).closedInterior = affineSegment R (s.points i) (s.points j)$$

Lean4

/-- A point lies in the closed interior of a 1-simplex if and only if it lies weakly between its
vertices. -/
theorem mem_closedInterior_iff_wbtw {s : Simplex R P 1} {p : P} :
    p ∈ s.closedInterior ↔ Wbtw R (s.points 0) p (s.points 1) := by rw [closedInterior_eq_affineSegment, Wbtw]

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