Finite preorders and finite sets in a preorder

This file shows that non-empty finite sets in a preorder have minimal/maximal elements, and contrapositively that non-empty sets without minimal or maximal elements are infinite.

It also provides uniqueness results for order embeddings and order homomorphisms on finite linear orders.

theorem Finset.exists_maximalFor {ι : Type u_1} {α : Type u_2} [LE α] [IsTrans α LE.le] (f : ι → α) (s : Finset ι) (hs : s.Nonempty) : ∃ (i : ι), MaximalFor (fun (x : ι) => x ∈ s) f i

theorem Finset.exists_minimalFor {ι : Type u_1} {α : Type u_2} [LE α] [IsTrans α fun (a a_1 : α) => a_1 ≤ a] (f : ι → α) (s : Finset ι) (hs : s.Nonempty) : ∃ (i : ι), MinimalFor (fun (x : ι) => x ∈ s) f i

theorem Finset.exists_maximal {α : Type u_2} [LE α] [IsTrans α LE.le] {s : Finset α} (hs : s.Nonempty) : ∃ (i : α), Maximal (fun (x : α) => x ∈ s) i

theorem Finset.exists_minimal {α : Type u_2} [LE α] [IsTrans α fun (a a_1 : α) => a_1 ≤ a] {s : Finset α} (hs : s.Nonempty) : ∃ (i : α), Minimal (fun (x : α) => x ∈ s) i

theorem Finset.exists_le_maximal {α : Type u_2} [Preorder α] {a : α} (s : Finset α) (ha : a ∈ s) : ∃ (b : α), a ≤ b ∧ Maximal (fun (x : α) => x ∈ s) b

theorem Finset.exists_le_minimal {α : Type u_2} [Preorder α] {a : α} (s : Finset α) (ha : a ∈ s) : ∃ b ≤ a, Minimal (fun (x : α) => x ∈ s) b

theorem Set.Finite.exists_maximalFor {ι : Type u_1} {α : Type u_2} [LE α] [IsTrans α LE.le] (f : ι → α) (s : Set ι) (h : s.Finite) (hs : s.Nonempty) : ∃ (i : ι), MaximalFor (fun (x : ι) => x ∈ s) f i

theorem Set.Finite.exists_minimalFor {ι : Type u_1} {α : Type u_2} [LE α] [IsTrans α fun (a a_1 : α) => a_1 ≤ a] (f : ι → α) (s : Set ι) (h : s.Finite) (hs : s.Nonempty) : ∃ (i : ι), MinimalFor (fun (x : ι) => x ∈ s) f i

theorem Set.Finite.exists_maximal {α : Type u_2} [LE α] [IsTrans α LE.le] {s : Set α} (h : s.Finite) (hs : s.Nonempty) : ∃ (i : α), Maximal (fun (x : α) => x ∈ s) i

theorem Set.Finite.exists_minimal {α : Type u_2} [LE α] [IsTrans α fun (a a_1 : α) => a_1 ≤ a] {s : Set α} (h : s.Finite) (hs : s.Nonempty) : ∃ (i : α), Minimal (fun (x : α) => x ∈ s) i

theorem Set.Finite.exists_maximalFor' {ι : Type u_1} {α : Type u_2} [LE α] [IsTrans α LE.le] (f : ι → α) (s : Set ι) (h : (f '' s).Finite) (hs : s.Nonempty) : ∃ (i : ι), MaximalFor (fun (x : ι) => x ∈ s) f i

A version of Finite.exists_maximalFor with the (weaker) hypothesis that the image of s is finite rather than s itself.

theorem Set.Finite.exists_minimalFor' {ι : Type u_1} {α : Type u_2} [LE α] [IsTrans α fun (a a_1 : α) => a_1 ≤ a] (f : ι → α) (s : Set ι) (h : (f '' s).Finite) (hs : s.Nonempty) : ∃ (i : ι), MinimalFor (fun (x : ι) => x ∈ s) f i

theorem Set.Finite.exists_le_maximal {α : Type u_2} [Preorder α] {s : Set α} {a : α} (hs : s.Finite) (ha : a ∈ s) : ∃ (b : α), a ≤ b ∧ Maximal (fun (x : α) => x ∈ s) b

theorem Set.Finite.exists_le_minimal {α : Type u_2} [Preorder α] {s : Set α} {a : α} (hs : s.Finite) (ha : a ∈ s) : ∃ b ≤ a, Minimal (fun (x : α) => x ∈ s) b

theorem Set.infinite_of_forall_exists_gt {α : Type u_2} [Preorder α] {s : Set α} [Nonempty α] (h : ∀ (a : α), ∃ b ∈ s, a < b) : s.Infinite

theorem Set.infinite_of_forall_exists_lt {α : Type u_2} [Preorder α] {s : Set α} [Nonempty α] (h : ∀ (a : α), ∃ b ∈ s, b < a) : s.Infinite

theorem Set.finite_isTop (α : Type u_2) [PartialOrder α] : {a : α | IsTop a}.Finite

theorem Set.finite_isBot (α : Type u_2) [PartialOrder α] : {a : α | IsBot a}.Finite

theorem Set.Infinite.exists_lt_map_eq_of_mapsTo {α : Type u_2} {β : Type u_3} [LinearOrder α] {s : Set α} {t : Set β} {f : α → β} (hs : s.Infinite) (hf : MapsTo f s t) (ht : t.Finite) : ∃ x ∈ s, ∃ y ∈ s, x < y ∧ f x = f y

theorem Set.Finite.exists_lt_map_eq_of_forall_mem {α : Type u_2} {β : Type u_3} [LinearOrder α] {t : Set β} {f : α → β} [Infinite α] (hf : ∀ (a : α), f a ∈ t) (ht : t.Finite) : ∃ (a : α) (b : α), a < b ∧ f a = f b

theorem Set.Finite.exists_subsingleton_isCofinal {α : Type u_2} [LinearOrder α] {s : Set α} (hs : s.Finite) (hs' : IsCofinal s) : ∃ (t : Set α), t.Subsingleton ∧ IsCofinal t

If the cofinality of a linear order is finite, it's at most one.

theorem Finite.exists_le_maximal {α : Type u_2} [Preorder α] [Finite α] {p : α → Prop} {a : α} (h : p a) : ∃ (b : α), a ≤ b ∧ Maximal p b

theorem Finite.exists_le_minimal {α : Type u_2} [Preorder α] [Finite α] {p : α → Prop} {a : α} (h : p a) : ∃ b ≤ a, Minimal p b

@[deprecated "Use `WellFoundedLT.induction _ h` instead." (since := "2026-04-10")]

theorem LinearOrder.strong_induction_of_finite {α : Type u_4} [LinearOrder α] [Finite α] {motive : α → Prop} (h : ∀ (j : α), (∀ k < j, motive k) → motive j) (i : α) : motive i

theorem OrderEmbedding.range_eq_iff {α : Type u_4} {β : Type u_5} [LinearOrder α] [PartialOrder β] [Finite α] {f g : α ↪o β} : Set.range ⇑f = Set.range ⇑g ↔ f = g

theorem OrderHom.range_eq_iff {α : Type u_4} {β : Type u_5} [LinearOrder α] [PartialOrder β] [Finite α] {f g : α →o β} (hf : Function.Injective ⇑f) (hg : Function.Injective ⇑g) : Set.range ⇑f = Set.range ⇑g ↔ f = g

theorem OrderHom.eq_id_of_injective {α : Type u_4} [LinearOrder α] [Finite α] (f : α →o α) (hf : Function.Injective ⇑f) : f = id

theorem StrictMono.eq_id {α : Type u_4} [LinearOrder α] [Finite α] {f : α → α} (hf : StrictMono f) : f = id

A strictly monotone self-map of a finite linear order is the identity.

theorem StrictMono.apply_eq {α : Type u_4} [LinearOrder α] [Finite α] {f : α → α} {x : α} (hf : StrictMono f) : f x = x

A strictly monotone self-map of a finite linear order fixes every point.