English
If S is bounded above in a linear order with archimedean property, then there exists a greatest element of S.
Русский
Пусть S ограничено сверху; тогда существует наибольший элемент множества S.
LaTeX
$$$ \text{BddAbove}(S) \land S \neq \emptyset \Rightarrow \exists x, IsGreatest(S,x).$$$
Lean4
theorem exists_isGreatest_of_nonempty {X : Type*} [LinearOrder X] [SuccOrder X] [IsSuccArchimedean X] {S : Set X}
(hS : BddAbove S) (hS' : S.Nonempty) : ∃ x, IsGreatest S x :=
by
obtain ⟨m, hm⟩ := hS
obtain ⟨n, hn⟩ := hS'
by_cases hm' : m ∈ S
· exact ⟨_, hm', hm⟩
have hn' := hm hn
revert hn hm hm'
refine Succ.rec ?_ ?_ hn'
· simp +contextual
intro m _ IH hm hn hm'
rw [mem_upperBounds] at IH hm
simp_rw [Order.le_succ_iff_eq_or_le] at hm
replace hm : ∀ x ∈ S, x ≤ m := by
intro x hx
refine (hm x hx).resolve_left ?_
rintro rfl
exact hm' hx
by_cases hmS : m ∈ S
· exact ⟨m, hmS, hm⟩
· exact IH hm hn hmS
