ite_ae_eq_of_measure_compl_zero — Mathlib

English

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

Русский

Если μ(сопряжённое отношение) μ(сеп) = 0, то функция x ↦ если x ∈ s тогда f(x) иначе g(x) равна μ-почти что f.

LaTeX

$$$(\mu(s^c) = 0) \Rightarrow (x \mapsto \mathrm{ite}(x \in s, f(x), g(x))) =_μ f$$$

Lean4

theorem ite_ae_eq_of_measure_compl_zero {γ} (f : α → γ) (g : α → γ) (s : Set α) [DecidablePred (· ∈ s)]
    (hs_zero : μ sᶜ = 0) : (fun x => ite (x ∈ s) (f x) (g x)) =ᵐ[μ] f :=
  by
  rw [← mem_ae_iff] at hs_zero
  filter_upwards [hs_zero]
  intros
  split_ifs
  rfl

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