orderTop — Mathlib

English

If a is the greatest element of s, then the suborder on s has a top element given by a.

Русский

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

LaTeX

$$$$ IsGreatest(s,a) \Rightarrow \text{OrderTop } s.\mathrm{Elem} $$$$

Lean4

/-- If `a` is the greatest element of a set `s`, then subtype `s` is an order with top element. -/
abbrev orderTop (h : IsGreatest s a) : OrderTop s
    where
  top := ⟨a, h.1⟩
  le_top := Subtype.forall.2 h.2

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