wbtw_const_sub_iff

Mathlib.Analysis.Convex.Between

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

English

A fixed subtraction from all three points preserves Wbtw: Wbtw R (p - x) (p - y) (p - z) iff Wbtw R x y z.

Русский

Фиксированное вычитание из всех трёх точек сохраняет Wbtw.

LaTeX

$$Wbtw R (p - x) (p - y) (p - z) \iff Wbtw R x y z$$

Lean4

@[simp]
theorem wbtw_const_sub_iff {x y z : V} (v : V) : Wbtw R (v - x) (v - y) (v - z) ↔ Wbtw R x y z :=
  wbtw_const_vsub_iff v

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

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

Разделы

Аффилиация

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