restrict_piecewise_compl — Mathlib

English

Restriction to the complement of a set of a piecewise function equals restricting to the complement of g.

Русский

Ограничение до дополнения множества от piecewise f g равно ограничению до дополнения для g.

LaTeX

$$$s^{c}.restrict (\\text{piecewise } s f g) = s^{c}.restrict g$$

Lean4

@[simp]
theorem restrict_piecewise_compl (f g : α → β) (s : Set α) [∀ x, Decidable (x ∈ s)] :
    sᶜ.restrict (piecewise s f g) = sᶜ.restrict g :=
  restrict_ite_compl _ _ _

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