restrict_ite_compl — Mathlib

English

Similar to the previous fact, but restricted to the complement: the restriction of the piecewise function to the complement equals the restriction to the complement of g.

Русский

Аналогично предыдущему, но ограничение на дополнение даёт: ограничение по дополнению от функции с кусочно-границей равно ограничению по дополнению для g.

LaTeX

$$$\\bigl(s^{c}\\restrict (\\lambda a. \\text{ite } (a \\in s) (f\\,a) (g\\,a))\\bigr) = s^{c}\\restrict g$$

Lean4

@[simp]
theorem restrict_ite_compl (f g : α → β) (s : Set α) [∀ x, Decidable (x ∈ s)] :
    (sᶜ.restrict fun a => if a ∈ s then f a else g a) = sᶜ.restrict g :=
  restrict_dite_compl _ _

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