instInfTopHomClass — Mathlib

English

There is a class structure that equips InfTopHom α β with the ability to map infimum and top elements via operations map_inf and map_top.

Русский

Существует структура класса, которая наделяет InfTopHom α β свойствами сохранения наименьших элементов и верхних элементов через map_inf и map_top.

LaTeX

$$$\\mathrm{InfTopHomClass}(\\mathrm{InfTopHom}(\\alpha,\\beta),\\alpha,\\beta)$ with $\\mathrm{map\\_inf}(f)=f.map\\_inf'$ and $\\mathrm{map\\_top}(f)=f.map\\_top'$$$

Lean4

instance : InfTopHomClass (InfTopHom α β) α β
    where
  map_inf f := f.map_inf'
  map_top f := f.map_top'

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