toInfHomClass — Mathlib

English

If α and β are lattices and F is a lattice hom class, then F is an InfHomClass.

Русский

Если α и β — решетки и F — класс гомоморфизмов решетки, то F — InfHomClass.

LaTeX

$$$$ [Lattice α] [Lattice β] [LatticeHomClass F α β] \Rightarrow \mathrm{InfHomClass} F α β. $$$$

Lean4

instance (priority := 100) toInfHomClass [Lattice α] [Lattice β] [LatticeHomClass F α β] : InfHomClass F α β :=
  { ‹LatticeHomClass F α β› with }

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