generateSetAlgebra_subset_self — Mathlib

English

If 𝒜 is an algebra of sets, then generateSetAlgebra 𝒜 ⊆ 𝒜.

Русский

Если 𝒜 — алгебра множеств, то generateSetAlgebra 𝒜 ⊆ 𝒜.

LaTeX

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

Lean4

/-- If `𝒜` is an algebra of sets, then it contains the algebra generated by itself. -/
theorem generateSetAlgebra_subset_self (h𝒜 : IsSetAlgebra 𝒜) : generateSetAlgebra 𝒜 ⊆ 𝒜 :=
  h𝒜.generateSetAlgebra_subset subset_rfl

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