coe_withTop

Mathlib.Order.Hom.WithTopBot

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

English

The underlying function of f.withTop coincides with the top-extended map on f.

Русский

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

LaTeX

$$$ \text{⇑}f.{\mathrm{withTop}} = \mathrm{WithTop.map} f $$$

Lean4

@[simp, norm_cast]
theorem coe_withTop (f : LatticeHom α β) : ⇑f.withTop = WithTop.map f :=
  rfl

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

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

Разделы

Аффилиация

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