English
For any two functions f, g on α and any set s, restricting the function a ↦ if a ∈ s then f a else g a to s equals restricting f to s.
Русский
Для любых функций f, g на α и множества s выполнено: ограничение функции a ↦ если a ∈ s тогда f a иначе g a до s эквивалентно ограничению f до s.
LaTeX
$$$\\bigl(s\\restrict (\\lambda a. \\text{ite } (a \\in s) (f\\,a) (g\\,a))\\bigr) = s\\restrict f$$
Lean4
@[simp]
theorem restrict_ite (f g : α → β) (s : Set α) [∀ x, Decidable (x ∈ s)] :
(s.restrict fun a => if a ∈ s then f a else g a) = s.restrict f :=
restrict_dite _ _