isGreatest_top_iff — Mathlib

English

In a preorder with a top element, s has ⊤ as a greatest element if and only if ⊤ ∈ s.

Русский

В предпорядке с верхней границей множество s имеет ⊤ как наибольший элемент тогда и только тогда, когда ⊤ ∈ s.

LaTeX

$$$\\IsGreatest s \\top \\iff \\top \\in s$$$

Lean4

@[simp]
theorem isGreatest_top_iff [OrderTop α] : IsGreatest s ⊤ ↔ ⊤ ∈ s :=
  and_iff_left <| top_mem_upperBounds _

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