constPi — Mathlib

English

The map constPi: β → C(α, β) assigns to each b ∈ β the constant function α → β with value b.

Русский

Отображение constPi: β → C(α, β) отправляет каждый b ∈ β в константную функцию α → β, принимающую значение b.

LaTeX

$$$\operatorname{constPi} : C(β, α \to β),\quad \operatorname{toFun}(\operatorname{constPi})(b) = \lambda a. b$$$

Lean4

/-- `Function.const α b` as a bundled continuous function of `b`. -/
@[simps -fullyApplied]
def constPi : C(β, α → β) where toFun b := Function.const α b

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