piecewise — Mathlib

English

Combine functions with disjoint domains into a single function by setting (piecewise f)(x) = f(hs.index x)(x).

Русский

Объединение функций с непересекающимися доменами в одну функцию: (piecewise f)(x) = f(hs.index x)(x).

LaTeX

$$$ \text{piecewise}_{hs} f \;: \; \alpha \to \beta \quad \text{defined by} \quad (\text{piecewise}_{hs} f)(x) = f (hs.index x)\, x $$$

Lean4

/-- Combine functions with disjoint domains into a new function.
You can use the regular expression `def.*piecewise` to search for
other ways to define piecewise functions in mathlib4. -/
def piecewise {β : Type*} (f : ι → α → β) : α → β := fun x => f (hs.index x) x

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