toCompleteLatticeHomClass — Mathlib

English

There is a mechanism to view order isomorphisms as complete lattice homomorphisms.

Русский

Существует способ рассматривать изоморфизмы порядка как гомоморфизмы полной решетки.

LaTeX

$$$ \\text{OrderIsoClass } F \\Rightarrow \\text{CompleteLatticeHomClass } F$$$

Lean4

instance (priority := 100) toCompleteLatticeHomClass [CompleteLattice α] [CompleteLattice β] [OrderIsoClass F α β] :
    CompleteLatticeHomClass F α β :=
  { OrderIsoClass.tosSupHomClass, OrderIsoClass.tosInfHomClass with }

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