coe_withBot

Mathlib.Order.Hom.WithTopBot

URI: https://scilib.ai/kg/mathlib#LatticeHom.coe_withBot

English

The underlying function of f.withBot coincides with the bottom-extended map on f.

Русский

Функциональная часть f.withBot совпадает с нижним расширением отображения f.

LaTeX

$$$ \text{⇑}f.{\mathrm{withBot}} = \mathrm{WithBot.map} f $$$

Lean4

@[simp, norm_cast]
theorem coe_withBot (f : LatticeHom α β) : ⇑f.withBot = WithBot.map f :=
  rfl

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

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

Разделы

Аффилиация

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