English
If s =ᵐ[comap f μ] t (i.e., s and t are almost everywhere equal with respect to comap f μ), then f''s =ᵐ[μ] f''t (their images are equal almost everywhere with respect to μ).
Русский
Если множества s и t равны почти в смысле comap f μ, то их образы под f совпадают почти в смысле μ.
LaTeX
$$$s =^{\\ae}_{comp f μ} t \\Rightarrow f''s =^{\\ae}_{μ} f''t$$$
Lean4
theorem ae_eq_image_of_ae_eq_comap (f : α → β) (μ : Measure β) (hfi : Injective f)
(hf : ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) μ) {s t : Set α} (hst : s =ᵐ[comap f μ] t) :
f '' s =ᵐ[μ] f '' t := by
rw [EventuallyEq, ae_iff] at hst ⊢
have h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s := by
ext1 x
simp only [eq_iff_iff, mem_setOf_eq, mem_union, mem_diff]
tauto
have h_eq_β : {a : β | ¬(f '' s) a = (f '' t) a} = f '' s \ f '' t ∪ f '' t \ f '' s :=
by
ext1 x
simp only [eq_iff_iff, mem_setOf_eq, mem_union, mem_diff]
tauto
rw [← Set.image_diff hfi, ← Set.image_diff hfi, ← Set.image_union] at h_eq_β
rw [h_eq_β]
rw [h_eq_α] at hst
exact measure_image_eq_zero_of_comap_eq_zero f μ hfi hf hst
