sbtw_mul_sub_add_iff

Mathlib.Analysis.Convex.Between

URI: https://scilib.ai/kg/mathlib#sbtw_mul_sub_add_iff

← MathLib Explorer

English

For x,y,r ∈ R, Sbtw R x (r·(y−x) + x) y holds exactly when x ≠ y and r ∈ (0,1).

Русский

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

LaTeX

$$$$ \text{Sbtw } R x (r \cdot (y - x) + x) y \iff x \neq y \land r \in (0,1) $$$$

Lean4

@[simp]
theorem sbtw_mul_sub_add_iff [NoZeroDivisors R] {x y r : R} :
    Sbtw R x (r * (y - x) + x) y ↔ x ≠ y ∧ r ∈ Set.Ioo (0 : R) 1 :=
  sbtw_lineMap_iff

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru