instOrderBotShrink — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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