IicExtend — Mathlib

English

Extend a function defined on (-∞, b] to a map α → β by composing with the projection to (-∞, b].

Русский

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

LaTeX

$$$\mathrm{IicExtend} \; (f) = f \circ \mathrm{projIic}(b)$$$

Lean4

/-- Extend a function `(-∞, b] → β` to a map `α → β`. -/
def IicExtend (f : Iic b → β) : α → β :=
  f ∘ projIic b

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