orderBot — Mathlib

English

If a is the least element of s, then the suborder on s has a bottom element given by a.

Русский

Если a является наименьшим элементом множества s, то у подотряда s есть нижняя грань, заданная a.

LaTeX

$$$$ IsLeast(s,a) \Rightarrow \text{OrderBot } s.\mathrm{Elem} \text{ with bottom } (a,h.1) \text{ and } (h.2). $$$$

Lean4

/-- If `a` is the least element of a set `s`, then subtype `s` is an order with bottom element. -/
abbrev orderBot (h : IsLeast s a) : OrderBot s where
  bot := ⟨a, h.1⟩
  bot_le := Subtype.forall.2 h.2

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