piecewise_comp — Mathlib

English

For any s ⊆ α and function h, the piecewise composition satisfies: (piecewise_s f g) ∘ h = piecewise_{h^{-1}(s)} (f ∘ h) (g ∘ h).

Русский

Для любого s ⊆ α и функции h: (piecewise_s f g) ∘ h = piecewise_{h^{-1}(s)} (f ∘ h) (g ∘ h).

LaTeX

$$$\\mathrm{piecewise}_{s} f g \\circ h = \\mathrm{piecewise}_{h^{-1}(s)} (f \\circ h) (g \\circ h)$$$

Lean4

theorem piecewise_comp (f g : α → γ) (h : β → α) :
    letI : DecidablePred (· ∈ h ⁻¹' s) := @instDecidablePredComp _ (· ∈ s) _ h _;
    (s.piecewise f g) ∘ h = (h ⁻¹' s).piecewise (f ∘ h) (g ∘ h) :=
  rfl

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