Finite_Non_Empty_Subset_of_Totally_Ordered_Set_has_Smallest_and_Greatest_Elements

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

finite-non-empty-subset-of-totally-ordered-set-has-smallest-and-greatest-elementsproofwikitotal-orderings

Let $\left({S, \preceq}\right)$ be a totally ordered set. Then every finite $T$ such that $\varnothing \subset T \subseteq S$ has both a smallest and a greatest element.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Finite_Non_Empty_Subset_of_Totally_Ordered_Set_has_Smallest_and_Greatest_Elements (T : Finset ℤ) (hT : T.Nonempty) : ∃ a, a ∈ T ∧ ∀ x, x ∈ T → a ≤ x := by sorry

Source

https://proofwiki.org/wiki/Finite_Non-Empty_Subset_of_Totally_Ordered_Set_has_Smallest_and_Greatest_Elements

View graph