isSetAlgebra_generateSetAlgebra — Mathlib

English

The algebra generated by 𝒜 contains 𝒜.

Русский

Алгебра, порожденная 𝒜, содержит 𝒜.

LaTeX

$$$𝒜 \\subseteq \\operatorname{generateSetAlgebra} 𝒜$$$

Lean4

/-- The algebra of sets generated by a family of sets is an algebra of sets. -/
theorem isSetAlgebra_generateSetAlgebra : IsSetAlgebra (generateSetAlgebra 𝒜)
    where
  empty_mem := generateSetAlgebra.empty
  compl_mem := fun _ hs ↦ generateSetAlgebra.compl _ hs
  union_mem := fun _ _ hs ht ↦ generateSetAlgebra.union _ _ hs ht

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