coe_withTopWithBot

Mathlib.Order.Hom.WithTopBot

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

English

The coercion of withTopWithBot is the same as applying WithTop.map to WithBot.map f.

Русский

Коэрциaция withTopWithBot равна применению WithTop.map к WithBot.map f.

LaTeX

$$$ \\boxed{\\; f.\\mathrm{withTopWithBot} = \\mathrm{WithTop.map}(\\mathrm{WithBot.map} f) \\}$$$

Lean4

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

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

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

Разделы

Аффилиация

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