toBotHomClass — Mathlib

English

Given a bounded-order homomorphism class, there is a BotHomClass structure on F α β.

Русский

При наличии класса гомоморфизмов ограниченного порядка существует структура BotHomClass для F α β.

LaTeX

$$$ BotHomClass\ F\ α\ β $$$

Lean4

instance (priority := 100) toBotHomClass [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] [BoundedOrderHomClass F α β] :
    BotHomClass F α β :=
  { ‹BoundedOrderHomClass F α β› with }

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