piecewise_eqOn

Mathlib.Data.Set.Piecewise

URI: https://scilib.ai/kg/mathlib#Set.piecewise_eqOn

English

EqOn (s.piecewise f g) f s, i.e., on s the piecewise function agrees with f.

Русский

EqOn (s.piecewise f g) f s: на тождестве s функция piecewise совпадает с f.

LaTeX

$$$\\forall i\\in s,\\ (s.\\mathrm{piecewise} f g)(i) = f(i)$$$

Lean4

theorem piecewise_eqOn (f g : α → β) : EqOn (s.piecewise f g) f s := fun _ => piecewise_eq_of_mem _ _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru