coeTail

Mathlib.Order.Filter.Germ.Basic

URI: https://scilib.ai/kg/mathlib#Filter.Germ.coeTail

English

There is a CoeTail from β to Germ l β given by the germ of the constant function.

Русский

Существует отображение из β в Germ l β задаваемое константным жерменом.

LaTeX

$$$\mathrm{coeTail} : \mathrm{CoeTail}(\beta, \mathrm{Germ}(l, \beta))\;\; (b \mapsto \mathrm{const}(l,b)).$$$

Lean4

instance coeTail : CoeTail β (Germ l β) :=
  ⟨const⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru