toBoundedLatticeHomClass — Mathlib

English

Frame homomorphisms induce bounded lattice homomorphisms.

Русский

Гомоморфизмы фрейма индуцируют гомоморфизмы ограниченных решеток.

LaTeX

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

Lean4

instance (priority := 100) toBoundedLatticeHomClass [CompleteLattice α] [CompleteLattice β] [FrameHomClass F α β] :
    BoundedLatticeHomClass F α β :=
  { ‹FrameHomClass F α β›, sSupHomClass.toSupBotHomClass with }
    -- See note [lower instance priority]

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