ite_ae_eq_of_measure_zero — Mathlib

English

If μ(s) = 0, then the function x ↦ if x ∈ s then f(x) else g(x) is μ-almost everywhere equal to g.

Русский

Если μ(s) = 0, тогда функция x ↦ 1_{s}(x) f(x) + 1_{s^c}(x) g(x) равна μ-почти что g.

LaTeX

$$$(\mu(s) = 0) \Rightarrow (x \mapsto \mathbf{1}_s(x) f(x) + (1-\mathbf{1}_s(x)) g(x)) =_μ g$$$

Lean4

theorem ite_ae_eq_of_measure_zero {γ} (f : α → γ) (g : α → γ) (s : Set α) [DecidablePred (· ∈ s)] (hs_zero : μ s = 0) :
    (fun x => ite (x ∈ s) (f x) (g x)) =ᵐ[μ] g :=
  by
  have h_ss : sᶜ ⊆ {a : α | ite (a ∈ s) (f a) (g a) = g a} := fun x hx => by simp [(Set.mem_compl_iff _ _).mp hx]
  refine measure_mono_null ?_ hs_zero
  conv_rhs => rw [← compl_compl s]
  rwa [Set.compl_subset_compl]

Похожие утверждения