instBoundedLatticeHomClass — Mathlib

English

There is a BoundedLatticeHomClass instance for bounding lattice homomorphisms, specifying map_sup, map_inf, map_top, map_bot.

Русский

Существует инстанс BoundedLatticeHomClass для гомоморфизмов ограниченной решетки, задающий map_sup, map_inf, map_top, map_bot.

LaTeX

$$$\\text{instBoundedLatticeHomClass}:\\mathrm{BoundedLatticeHomClass}(\\mathrm{BoundedLatticeHom}(\\alpha,\\beta),\\alpha,\\beta)$ with $\\text{map\\_sup}(f)=f.map\\_sup'$, $\\text{map\\_inf}(f)=f.map\\_inf'$, $\\text{map\\_top}(f)=f.map\\_top'$, $\\text{map\\_bot}(f)=f.map\\_bot'$$$

Lean4

instance instBoundedLatticeHomClass : BoundedLatticeHomClass (BoundedLatticeHom α β) α β
    where
  map_sup f := f.map_sup'
  map_inf f := f.map_inf'
  map_top f := f.map_top'
  map_bot f := f.map_bot'

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