toSupBotHomClass — Mathlib

English

From an order isomorphism class, one obtains a SupBotHomClass between α and β.

Русский

Из класса биекций порядков получаем SupBotHomClass между α и β.

LaTeX

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

Lean4

instance (priority := 100) toSupBotHomClass [SemilatticeSup α] [OrderBot α] [SemilatticeSup β] [OrderBot β]
    [OrderIsoClass F α β] : SupBotHomClass F α β :=
  { OrderIsoClass.toSupHomClass, OrderIsoClass.toBotHomClass with }
    -- See note [lower instance priority]

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