const — Mathlib

English

The germ of a constant function b: α→β is the same as the germ of the constant germ function in Germ l β.

Русский

Жермен константы b есть константный жерм функции в Germ l β.

LaTeX

$$$\mathrm{const}(l, b) : \mathrm{Germ}(l, \beta)\quad\text{defined as }\mathrm{ofFun}(\lambda a. b).$$$

Lean4

/-- Germ of the constant function `fun x : α ↦ c` at a filter `l`. -/
@[coe]
def const {l : Filter α} (b : β) : (Germ l β) :=
  ofFun fun _ => b

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