feat: the sigma-algebra generated by the constant indicator of a set is smaller than the one generated by the set (leanprover-community#39753)

This PR was automatically created from PR leanprover-community#37259 by @EtienneC30 via a [review comment](leanprover-community#37259 (comment)) by @EtienneC30.

Co-authored-by: EtienneC30 <66847262+EtienneC30@users.noreply.github.com>
Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>

Author: 2 people

Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean

@@ -42,6 +42,12 @@ lemma generateFrom_singleton_le {m : MeasurableSpace α} {s : Set α} (hs : Meas
     MeasurableSpace.generateFrom {s} ≤ m :=
   generateFrom_le (fun _ ht ↦ mem_singleton_iff.1 ht ▸ hs)
 
+lemma comap_indicator_const_le_generateFrom_singleton {M : Type*} [Zero M] [MeasurableSpace M]
+    (s : Set α) (c : M) :
+    MeasurableSpace.comap (s.indicator (fun _ ↦ c)) inferInstance ≤
+      MeasurableSpace.generateFrom {s} :=
+  (measurable_const.indicator (measurableSet_generateFrom (by simp))).comap_le
+
 end MeasurableSpace
 
 namespace MeasureTheory