toBoundedLatticeHomClass — Mathlib

English

From an order isomorphism class, obtain a bounded-lattice-hom-class.

Русский

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

LaTeX

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

Lean4

instance (priority := 100) toBoundedLatticeHomClass [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β]
    [OrderIsoClass F α β] : BoundedLatticeHomClass F α β :=
  { OrderIsoClass.toLatticeHomClass, OrderIsoClass.toBoundedOrderHomClass with }

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