instCoeTCLatticeHomOfLatticeHomClass

English

There is a canonical coercion from F to a lattice homomorphism when α and β are lattices and F is a lattice hom class.

Русский

Существует каноническое приведение из F к гомоморфизму решетки, если α и β — решетки и F — класс гомоморфизмов решетки.

LaTeX

$$$$ [\text{Lattice } \alpha] [\text{Lattice } \beta] [\text{LatticeHomClass } F \alpha \beta] \Rightarrow \mathrm{CoeTC} F (\mathrm{LatticeHom} \alpha \beta). $$$$

Lean4

instance [Lattice α] [Lattice β] [LatticeHomClass F α β] : CoeTC F (LatticeHom α β) :=
  ⟨fun f =>
    { toFun := f
      map_sup' := map_sup f
      map_inf' := map_inf f }⟩

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