piecewise_ite — Mathlib

English

Let f, f', g be functions α→β and t, t' subsets of α. If EqOn f g on t and EqOn f' g on t' hold, then EqOn (s.piecewise f f') g on s.ite t t'.

Русский

Пусть f, f', g — функции α→β, и t, t' — подмножества α. ЕслиEqOn f g на t и EqOn f' g на t' выполнены, тогда EqOn (s.piecewise f f') g на s.ite t t'.

LaTeX

$$$EqOn f g t \\to EqOn f' g t' \\to EqOn (s.piecewise f f') g (s.ite t t')$$$

Lean4

theorem piecewise_ite {f f' g : α → β} {t t'} (h : EqOn f g t) (h' : EqOn f' g t') :
    EqOn (s.piecewise f f') g (s.ite t t') :=
  (h.mono inter_subset_left).piecewise_ite' s (h'.mono inter_subset_left)

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