toInfTopHomClass — Mathlib

English

From an order iso class, obtain an InfTopHomClass.

Русский

Из класса изоморфизмов порядков получают InfTopHomClass.

LaTeX

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

Lean4

instance (priority := 100) toInfTopHomClass [SemilatticeInf α] [OrderTop α] [SemilatticeInf β] [OrderTop β]
    [OrderIsoClass F α β] : InfTopHomClass F α β :=
  { OrderIsoClass.toInfHomClass, OrderIsoClass.toTopHomClass with }
    -- See note [lower instance priority]

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