toLatticeHomClass — Mathlib

English

Given an order isomorphism, one obtains a LatticeHomClass between the underlying lattices.

Русский

Дана изоморфия порядка; получается LatticeHomClass между решетками.

LaTeX

$$$$ [\text{Lattice }\alpha] [\text{Lattice }\beta] [\mathrm{OrderIsoClass } F \alpha \beta] \Rightarrow \mathrm{LatticeHomClass} F \alpha \beta. $$$$

Lean4

instance (priority := 100) toLatticeHomClass [Lattice α] [Lattice β] [OrderIsoClass F α β] : LatticeHomClass F α β :=
  { OrderIsoClass.toSupHomClass, OrderIsoClass.toInfHomClass with }

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