restrict_ite — Mathlib

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 _ _

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