toTopHomClass — Mathlib

English

From InfTopHomClass, one obtains TopHomClass when working with lattices and top elements.

Русский

Из InfTopHomClass получаем TopHomClass в контексте решеток с верхом.

LaTeX

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

Lean4

instance (priority := 100) toTopHomClass [Min α] [Min β] [Top α] [Top β] [InfTopHomClass F α β] : TopHomClass F α β :=
  { ‹InfTopHomClass F α β› with }
    -- See note [lower instance priority]

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