English
If 𝒜 ⊆ ℬ and ℬ is an algebra, then generateSetAlgebra 𝒜 ⊆ ℬ.
Русский
Если 𝒜 ⊆ ℬ и ℬ — алгебра, то generateSetAlgebra 𝒜 ⊆ ℬ.
LaTeX
$$$𝒜 ⊆ ℬ \\Rightarrow \\operatorname{generateSetAlgebra} 𝒜 ⊆ ℬ$$$
Lean4
/-- If a family of sets `𝒜` is contained in `ℬ`, then the algebra of sets generated by `𝒜`
is contained in the one generated by `ℬ`. -/
theorem generateSetAlgebra_mono {ℬ : Set (Set α)} (h : 𝒜 ⊆ ℬ) : generateSetAlgebra 𝒜 ⊆ generateSetAlgebra ℬ :=
by
intro s hs
induction hs with
| base t t_mem => exact self_subset_generateSetAlgebra (h t_mem)
| empty => exact isSetAlgebra_generateSetAlgebra.empty_mem
| compl t _ t_mem => exact isSetAlgebra_generateSetAlgebra.compl_mem t_mem
| union t u _ _ t_mem u_mem => exact isSetAlgebra_generateSetAlgebra.union_mem t_mem u_mem
