toFrameHomClass — Mathlib

English

Any complete lattice homomorphism class yields a frame homomorphism class.

Русский

Любой класс гомоморфизмов полной решетки образует класс гомоморфизмов фрейма.

LaTeX

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

Lean4

instance (priority := 100) toFrameHomClass [CompleteLattice α] [CompleteLattice β] [CompleteLatticeHomClass F α β] :
    FrameHomClass F α β :=
  { ‹CompleteLatticeHomClass F α β›, sInfHomClass.toInfTopHomClass with }
    -- See note [lower instance priority]

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