compl_subset_iff_union

Mathlib.Order.BooleanAlgebra.Set

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

← MathLib Explorer

English

sᶜ ⊆ t implies s ∪ t = univ; equivalently, sᶜ ⊆ t ⇔ s ∪ t = univ.

Русский

sᶜ ⊆ t тогда и только тогда, когда s ∪ t = univ.

LaTeX

$$$s^{c} \subseteq t \iff s \cup t = \mathrm{univ}$$$

Lean4

theorem compl_subset_iff_union {s t : Set α} : sᶜ ⊆ t ↔ s ∪ t = univ :=
  Iff.symm <| eq_univ_iff_forall.trans <| forall_congr' fun _ => or_iff_not_imp_left

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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