English
If f preserves μa→μb and g is null-measurable, then (g ∘ f) is ae-constant with respect to μa iff g is ae-constant with respect to μb.
Русский
Если f сохраняет μa→μb и g нулемасштабируема, то (g ∘ f) ae-константа относительно μa тогда и только тогда, когда g ae-константа относительно μb.
LaTeX
$$$\text{MeasurePreserving } f \; μ_a \; μ_b \rightarrow \forall g, \text{NullMeasurable } g\; μ_b \rightarrow (\text{ae-const }(g\circ f; μ_a) \iff \text{ae-const }(g; μ_b))$$$
Lean4
theorem aeconst_comp [MeasurableSingletonClass γ] {f : α → β} (hf : MeasurePreserving f μa μb) {g : β → γ}
(hg : NullMeasurable g μb) : Filter.EventuallyConst (g ∘ f) (ae μa) ↔ Filter.EventuallyConst g (ae μb) :=
exists_congr fun s ↦
and_congr_left fun hs ↦ by
simp only [Filter.mem_map, mem_ae_iff, ← hf.measure_preimage (hg hs.measurableSet).compl, preimage_comp,
preimage_compl]
