English
The measurable space generated by 𝒜 is the same as the one generated by generateSetAlgebra 𝒜.
Русский
Измеримое пространство, порожденное 𝒜, такое же, как и порожденное generateSetAlgebra 𝒜.
LaTeX
$$$ generateFrom (generateSetAlgebra 𝒜) = generateFrom 𝒜 $$$
Lean4
/-- The measurable space generated by a family of sets `𝒜` is the same as the one generated
by the algebra of sets generated by `𝒜`. -/
@[simp]
theorem generateFrom_generateSetAlgebra_eq : generateFrom (generateSetAlgebra 𝒜) = generateFrom 𝒜 :=
by
refine le_antisymm (fun s ms ↦ ?_) (generateFrom_mono self_subset_generateSetAlgebra)
induction s, ms using generateFrom_induction with
| hC t ht h =>
clear h
induction ht with
| base u u_mem => exact measurableSet_generateFrom u_mem
| empty => exact @MeasurableSet.empty _ (generateFrom 𝒜)
| compl u _ mu => exact mu.compl
| union u v _ _ mu mv => exact MeasurableSet.union mu mv
| empty => exact MeasurableSpace.measurableSet_empty _
| compl t _ ht => exact ht.compl
| iUnion t _ ht => exact .iUnion ht
