wbtw_neg_iff

Mathlib.Analysis.Convex.Between

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

English

Negation preserves the weak-between relation: Wbtw R (-x) (-y) (-z) holds iff Wbtw R x y z holds.

Русский

Отрицание сохраняет слабое между: Wbtw R(-x)(-y)(-z) эквивалентно Wbtw R x y z.

LaTeX

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

Lean4

@[simp]
theorem wbtw_neg_iff {x y z : V} : Wbtw R (-x) (-y) (-z) ↔ Wbtw R x y z := by simp only [← zero_sub, wbtw_const_sub_iff]

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

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

Разделы

Аффилиация

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