wbtw_lineMap_iff — Mathlib

English

For x,y ∈ P and r ∈ R, Wbtw R x (lineMap x y r) y holds exactly when x = y or r ∈ [0,1].

Русский

Для точек x,y ∈ P и скаляра r ∈ R, Wbtw R x (lineMap x y r) y верно тогда и только тогда, когда x = y или r ∈ [0,1].

LaTeX

$$$$ Wbtw R x (lineMap x y r) y \quad\text{iff}\quad x = y \lor r \in [0,1] $$$$

Lean4

@[simp]
theorem wbtw_lineMap_iff [NoZeroSMulDivisors R V] {x y : P} {r : R} :
    Wbtw R x (lineMap x y r) y ↔ x = y ∨ r ∈ Set.Icc (0 : R) 1 :=
  by
  by_cases hxy : x = y
  · rw [hxy, lineMap_same_apply]
    simp
  rw [or_iff_right hxy, Wbtw, affineSegment, (lineMap_injective R hxy).mem_set_image]

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