[Merged by Bors] - feat: the sigma-algebra generated by the constant indicator of a set is smaller than the one generated by the set#39753

mathlib-splicebot[bot] wants to merge 2 commits into

masterleanprover-community/mathlib4:masterfrom

splice-bot/pr-37259-Mathlib-MeasureTheory-MeasurableSpace-MeasurablyGenerated.lean-9e6d6fab22-y6ejcm8leanprover-community/mathlib4_copy:splice-bot/pr-37259-Mathlib-MeasureTheory-MeasurableSpace-MeasurablyGenerated.lean-9e6d6fab22-y6ejcm8Copy head branch name to clipboard