restrict_piecewise — Mathlib

English

Restricting a function to a set of the form piecewise s f g is the same as restricting f to that set.

Русский

Ограничение функции до множества, задаваемого piecewise s f g, эквивалентно ограничению f до этого множества.

LaTeX

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

Lean4

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

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