instOrderTopShrink — Mathlib

English

If α has a top element, Shrink(α) inherits an OrderTop structure via the order isomorphism.

Русский

Если у α есть верхняя граница, Shrink(α) наследует структуру OrderTop через порядок-изоморфизм.

LaTeX

$$$\text{OrderTop}(\operatorname{Shrink}(\alpha))$$$

Lean4

noncomputable instance [OrderTop α] : OrderTop (Shrink.{u} α) where
  le_top
    a := by simp only [← (orderIsoShrink.{u} α).symm.le_iff_le, orderIsoShrink_symm_apply, equivShrink_symm_top, le_top]

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