toTopHomClass — Mathlib

English

There is a TopHomClass structure on F α β when F is a order-isomorphism class with a top element.

Русский

Существуют структуры TopHomClass для F α β для класса изоморфизмов порядка с верхней границей.

LaTeX

$$$ TopHomClass\ F\ α\ β $$$

Lean4

instance (priority := 100) toTopHomClass [LE α] [OrderTop α] [PartialOrder β] [OrderTop β] [OrderIsoClass F α β] :
    TopHomClass F α β :=
  { show OrderHomClass F α β from inferInstance with map_top := fun f => top_le_iff.1 <| (map_inv_le_iff f).1 le_top }
    -- See note [lower instance priority]

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