piecewise_ite' — Mathlib

English

If f and g agree on t ∩ s and f' and g agree on t' ∩ sᶜ, then the piecewise function s.piecewise f f' agrees with g on s.ite t t'.

Русский

Если f и g согласны на t ∩ s, а f' и g — на t' ∩ sᶜ, то функция s.piecewise f f' совпадает с g на s.ite t t'.

LaTeX

$$$EqOn f g (t \\cap s) \\land EqOn f' g (t' \\cap s^{c}) \\Rightarrow EqOn (s.piecewise f f') g (s.ite t t')$$$

Lean4

theorem piecewise_ite' {f f' g : α → β} {t t'} (h : EqOn f g (t ∩ s)) (h' : EqOn f' g (t' ∩ sᶜ)) :
    EqOn (s.piecewise f f') g (s.ite t t') := by simp [eqOn_piecewise, *]

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