univ_mem

Mathlib.MeasureTheory.SetAlgebra

URI: https://scilib.ai/kg/mathlib#MeasureTheory.IsSetAlgebra.univ_mem

English

An algebra of sets contains the universe.

Русский

Алгебра множеств содержит всё множество.

LaTeX

$$$\\text{univ} \\in 𝒜$$$

Lean4

/-- An algebra of sets contains the whole set. -/
theorem univ_mem (h𝒜 : IsSetAlgebra 𝒜) : univ ∈ 𝒜 :=
  compl_empty ▸ h𝒜.compl_mem h𝒜.empty_mem

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

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

Разделы

Аффилиация

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