piecewise_ae_eq_of_ae_eq_set — Mathlib

English

If s and t are ae-equal, then piecewise f g on s and t give the same ae-equality.

Русский

Если множества s и t равны почти повсюду, то соответствующие кусочные функции имеют одинаковое ae-равенство.

LaTeX

$$$ s =^\\mathrm{ae}_{\\mu} t \\Rightarrow s\\text{.piecewise } f g =^\\mathrm{ae}_{\\mu} t\\text{.piecewise } f g $$$

Lean4

theorem piecewise_ae_eq_of_ae_eq_set [DecidablePred (· ∈ s)] [DecidablePred (· ∈ t)] (hst : s =ᵐ[μ] t) :
    s.piecewise f g =ᵐ[μ] t.piecewise f g :=
  hst.mem_iff.mono fun x hx => by simp [piecewise, hx]

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