English
Subsets behave compatibly under restriction: NullMeasurableSet t (μ.restrict s) is equivalent to NullMeasurableSet t μ when t ⊆ s.
Русский
Подмножества ведут себя согласованно при ограничении: NullMeasurableSet t (μ.restrict s) эквивалентно NullMeasurableSet t μ, если t ⊆ s.
LaTeX
$$$ t \subseteq s \rightarrow (\text{NullMeasurableSet } t (μ.restrict s) \leftrightarrow \text{NullMeasurableSet } t μ). $$$
Lean4
theorem nullMeasurableSet_subtype_coe {t : Set s} (hs : NullMeasurableSet s μ) (ht : MeasurableSet t) :
NullMeasurableSet ((↑) '' t) μ :=
by
rw [Subtype.instMeasurableSpace, comap_eq_generateFrom] at ht
induction t, ht using generateFrom_induction with
| hC t' ht' =>
obtain ⟨s', hs', rfl⟩ := ht'
rw [Subtype.image_preimage_coe]
exact hs.inter (hs'.nullMeasurableSet)
| empty => simp only [image_empty, nullMeasurableSet_empty]
| compl t' _
ht' =>
simp only [← range_diff_image Subtype.coe_injective, Subtype.range_coe_subtype, setOf_mem_eq]
exact hs.diff ht'
| iUnion f _ hf =>
dsimp only []
rw [image_iUnion]
exact .iUnion hf
