sdiff_lt_left

Mathlib.Order.BooleanAlgebra.Basic

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

English

x \ y < x if and only if y is not disjoint from x.

Русский

x \ y < x тогда и только тогда, когда y не непересекается с x.

LaTeX

$$$x \setminus y < x \iff \neg Disjoint y x$$$

Lean4

theorem sdiff_lt_left : x \ y < x ↔ ¬Disjoint y x := by
  rw [lt_iff_le_and_ne, Ne, sdiff_eq_self_iff_disjoint, and_iff_right sdiff_le]

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

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

Разделы

Аффилиация

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