inter_compl_nonempty_iff

Mathlib.Order.BooleanAlgebra.Set

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

English

The set (s ∩ tᶜ) is nonempty if and only if s is not contained in t.

Русский

Множество (s ∩ tᶜ) непусто тогда, когда s не подмножество t.

LaTeX

$$$(s \cap t^{c}).Nonempty \iff \lnot (s \subseteq t)$$$

Lean4

theorem inter_compl_nonempty_iff {s t : Set α} : (s ∩ tᶜ).Nonempty ↔ ¬s ⊆ t :=
  (not_subset.trans <| exists_congr fun x => by simp).symm

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

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

Разделы

Аффилиация

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