diff_ssubset_left_iff

Mathlib.Order.BooleanAlgebra.Set

URI: https://scilib.ai/kg/mathlib#Set.diff_ssubset_left_iff

English

For sets S and T, (S \\ T) ⊊ S iff (S ∩ T) is Nonempty.

Русский

Для множеств S и T верно: (S \\ T) ⊊ S тогда и только тогда, когда S ∩ T непусто.

LaTeX

$$$ (S \\\\setminus T) \\\\subsetneq S \\\\Leftrightarrow (S \\\\cap T) \\\\neq \\\\emptyset $$$

Lean4

@[simp]
theorem diff_ssubset_left_iff : s \ t ⊂ s ↔ (s ∩ t).Nonempty :=
  sdiff_lt_left.trans <| by rw [not_disjoint_iff_nonempty_inter, inter_comm]

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

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

Разделы

Аффилиация

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