orderBot — Mathlib

English

If α has a bottom element, then Iic(a) has a bottom element, namely ⊥ (the bottom of α) living inside Iic(a).

Русский

Если в α существует наименьший элемент, то и в Iic(a) есть наименьший элемент, равный ⊥ в α, вложенный в Iic(a).

LaTeX

$$$$\\uparrow(\\bot_{\\mathrm{Iic}(a)}) = \\bot_{\\alpha}.$$$$

Lean4

instance orderBot [Preorder α] [OrderBot α] : OrderBot (Iic a)
    where
  bot := ⟨⊥, bot_le⟩
  bot_le := fun ⟨_, _⟩ => Subtype.mk_le_mk.2 bot_le

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