wbtw_mul_sub_add_iff — Mathlib

English

For x,y,r ∈ R (with NoZeroDivisors), Wbtw R x (r·(y−x) + x) y holds exactly when x = y or r ∈ [0,1].

Русский

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

LaTeX

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

Lean4

@[simp]
theorem wbtw_mul_sub_add_iff [NoZeroDivisors R] {x y r : R} :
    Wbtw R x (r * (y - x) + x) y ↔ x = y ∨ r ∈ Set.Icc (0 : R) 1 :=
  wbtw_lineMap_iff

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