IciExtend — Mathlib

English

Extend a function defined on the ray [a, ∞) to a map α → β by composing with the natural projection.

Русский

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

LaTeX

$$$\mathrm{IciExtend} \; (f) = f \circ \mathrm{projIci}(a)$$$

Lean4

/-- Extend a function `[a, ∞) → β` to a map `α → β`. -/
def IciExtend (f : Ici a → β) : α → β :=
  f ∘ projIci a

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