sup_eq_top_of_top_mem — Mathlib

English

If the top element ⊤ belongs to a set s in an OrderTop lattice, then the supremum of s is ⊤.

Русский

Если верхний элемент ⊤ принадлежит множеству s в порядке с верхней границей, то его супремум равен ⊤.

LaTeX

$$$ (\top \in s) \Rightarrow sSup s = \top $$$

Lean4

theorem sup_eq_top_of_top_mem [OrderTop α] (h : ⊤ ∈ s) : sSup s = ⊤ :=
  top_unique <| le_csSup (OrderTop.bddAbove s) h

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