generateSetAlgebra_subset — Mathlib

English

If 𝒜 ⊆ ℬ and ℬ is a set algebra, then generateSetAlgebra 𝒜 ⊆ ℬ.

Русский

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

LaTeX

$$$𝒜 ⊆ ℬ \\Rightarrow \\operatorname{generateSetAlgebra} 𝒜 ⊆ ℬ$$$

Lean4

/-- If a family of sets `𝒜` is contained in an algebra of sets `ℬ`, then so is the algebra of sets
generated by `𝒜`. -/
theorem generateSetAlgebra_subset {ℬ : Set (Set α)} (h : 𝒜 ⊆ ℬ) (hℬ : IsSetAlgebra ℬ) : generateSetAlgebra 𝒜 ⊆ ℬ :=
  by
  intro s hs
  induction hs with
  | base t t_mem => exact h t_mem
  | empty => exact hℬ.empty_mem
  | compl t _ t_mem => exact hℬ.compl_mem t_mem
  | union t u _ _ t_mem u_mem => exact hℬ.union_mem t_mem u_mem

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