sdiff_lt_left

Mathlib.Order.UpperLower.Closure

URI: https://scilib.ai/kg/mathlib#LowerSet.sdiff_lt_left

English

s.sdiff t is strictly below s iff s and t are not disjoint.

Русский

s.sdiff t меньше s строго тогда, когда s и t неразделимы.

LaTeX

$$$ s.sdiff t < s \\iff \\lnot Disjoint(s, t) $$$

Lean4

@[simp]
theorem sdiff_lt_left : s.sdiff t < s ↔ ¬Disjoint (↑s) t :=
  sdiff_le_left.lt_iff_ne.trans LowerSet.sdiff_eq_left.not

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

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

Разделы

Аффилиация

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