piecewise_congr — Mathlib

English

If f agrees with f' on s and g agrees with g' off s, then s.piecewise f g = s.piecewise f' g'.

Русский

Если f совпадает с f' на s и g совпадает с g' вне s, то s.piecewise f g = s.piecewise f' g'.

LaTeX

$$$(\\forall i \\in s, f i = f' i) \\land (\\forall i \\notin s, g i = g' i) \\Rightarrow s.\\text{piecewise } f g = s.\\text{piecewise } f' g'.$$$

Lean4

theorem piecewise_congr {f f' g g' : ∀ i, π i} (hf : ∀ i ∈ s, f i = f' i) (hg : ∀ i ∉ s, g i = g' i) :
    s.piecewise f g = s.piecewise f' g' :=
  funext fun i => if_ctx_congr Iff.rfl (hf i) (hg i)

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