IccExtend — Mathlib

English

Extend a function defined on [a, b] to a map α → β by composing with the projection onto [a,b].

Русский

Расширение функции, заданной на [a,b], до отображения α → β через проекцию на [a,b].

LaTeX

$$$\mathrm{IccExtend} \; (h) \; (f) = f \circ \mathrm{projIcc}(a,b,h)$$$

Lean4

/-- Extend a function `[a, b] → β` to a map `α → β`. -/
def IccExtend {a b : α} (h : a ≤ b) (f : Icc a b → β) : α → β :=
  f ∘ projIcc a b h

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