sbtw_pair

Mathlib.Analysis.Convex.BetweenList

URI: https://scilib.ai/kg/mathlib#List.sbtw_pair

English

A two-element list [p1, p2] satisfies Sbtw with respect to R if and only if p1 ≠ p2.

Русский

Двухэлементный список [p1, p2] удовлетворяет Sbtw тогда, когда p1 ≠ p2.

LaTeX

$$$Sbtw(R,[p_1,p_2]) \\iff p_1 \\neq p_2$$$

Lean4

@[simp]
theorem sbtw_pair {p₁ p₂ : P} : [p₁, p₂].Sbtw R ↔ p₁ ≠ p₂ := by simp [List.Sbtw]

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

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

Разделы

Аффилиация

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