toSupBotHomClass — Mathlib

English

From a bounded lattice homomorphism class on α,β one obtains a SupBotHomClass.

Русский

Из класса гомоморфизмов ограниченных решеток между α и β следует SupBotHomClass.

LaTeX

$$$\operatorname{BoundedLatticeHomClass}(F,\alpha,\beta) \Rightarrow \operatorname{SupBotHomClass}(F,\alpha,\beta)$$$

Lean4

instance (priority := 100) toSupBotHomClass [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β]
    [BoundedLatticeHomClass F α β] : SupBotHomClass F α β :=
  { ‹BoundedLatticeHomClass F α β› with }
    -- See note [lower instance priority]

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