lt_sdiff_left

Mathlib.Order.UpperLower.Closure

URI: https://scilib.ai/kg/mathlib#UpperSet.lt_sdiff_left

English

The strict order s < s.sdiff t is equivalent to not being disjoint with t.

Русский

Строгое неравенство s < s.sdiff t эквивалентно тому, что s и t не с непустым общим множеством.

LaTeX

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

Lean4

@[simp]
theorem lt_sdiff_left : s < s.sdiff t ↔ ¬Disjoint (↑s) t :=
  le_sdiff_left.lt_iff_ne'.trans UpperSet.sdiff_eq_left.not

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

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

Разделы

Аффилиация

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