toCompleteLatticeHom — Mathlib

English

An order isomorphism can be regarded as a complete lattice homomorphism.

Русский

Изоморфизм порядка может рассматриваться как гомоморфизм полной решетки.

LaTeX

$$$ \\text{OrderIso } \\alpha \\beta \\longrightarrow \\text{CompleteLatticeHom } \\alpha \\beta$$$

Lean4

/-- Reinterpret an order isomorphism as a morphism of complete lattices. -/
@[simps]
def toCompleteLatticeHom [CompleteLattice α] [CompleteLattice β] (f : OrderIso α β) : CompleteLatticeHom α β
    where
  toFun := f
  map_sInf' := sInfHomClass.map_sInf f
  map_sSup' := sSupHomClass.map_sSup f

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