sbtw_lineMap_iff — Mathlib

English

For x,y ∈ P and r ∈ R, Sbtw R x (lineMap x y r) y holds if and only if x ≠ y and r ∈ (0,1).

Русский

Для x,y ∈ P и r ∈ R, Sbtw R x (lineMap x y r) y верно тогда, когда x ≠ y и r ∈ (0,1).

LaTeX

$$$$ \text{Sbtw } R x (lineMap x y r) y \quad\leftrightarrow\quad x \neq y \land r \in (0,1) $$$$

Lean4

@[simp]
theorem sbtw_lineMap_iff [NoZeroSMulDivisors R V] {x y : P} {r : R} :
    Sbtw R x (lineMap x y r) y ↔ x ≠ y ∧ r ∈ Set.Ioo (0 : R) 1 :=
  by
  rw [sbtw_iff_mem_image_Ioo_and_ne, and_comm, and_congr_right]
  intro hxy
  rw [(lineMap_injective R hxy).mem_set_image]

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