toInfTopHom

Mathlib.Order.Hom.BoundedLattice

URI: https://scilib.ai/kg/mathlib#BoundedLatticeHom.toInfTopHom

English

There is a canonical reinterpretation from BoundLatticeHom to InfTopHom.

Русский

Существует каноническое преобразование из BoundLatticeHom в InfTopHom.

LaTeX

$$$\\text{toInfTopHom}(f):=\\mathrm{InfTopHom}(\\alpha,\\beta)$ for $f:\\mathrm{BoundedLatticeHom}(\\alpha,\\beta)$$$

Lean4

/-- Reinterpret a `BoundedLatticeHom` as an `InfTopHom`. -/
def toInfTopHom (f : BoundedLatticeHom α β) : InfTopHom α β :=
  { f with }

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

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

Разделы

Аффилиация

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