sdiff_eq_left

Mathlib.Order.UpperLower.Closure

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

English

s.sdiff t = s holds exactly when s is disjoint from t.

Русский

s.sdiff t = s тогда и только тогда, когда s и t не пересекаются.

LaTeX

$$$ s.sdiff t = s \\iff Disjoint(s, t) $$$

Lean4

@[simp]
protected theorem sdiff_eq_left : s.sdiff t = s ↔ Disjoint (↑s) t := by simp [← SetLike.coe_set_eq]

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

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

Разделы

Аффилиация

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