isGreatest_iff_eq — Mathlib

English

Let α be a partially ordered set and s a subset of α. If a is the greatest element of s, then any b that is a greatest element of s must equal a; equivalently, the greatest element of s is unique.

Русский

Пусть α — частично упорядоченное множество, s ⊆ α. Если a является наибольшим элементом множества s, то любой b, являющийся наибольшим элементом s, обязан быть равным a; то есть наибольший элемент множества уникален.

LaTeX

$$$ IsGreatest(s,a) \\rightarrow (IsGreatest(s,b) \\leftrightarrow a=b)$$$

Lean4

theorem isGreatest_iff_eq (Ha : IsGreatest s a) : IsGreatest s b ↔ a = b :=
  Iff.intro Ha.unique fun h => h ▸ Ha

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