# 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.

source
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
source
theorem Finset.exists_minimalFor {ι : Type u_1} {α : Type u_2} [LE α] [IsTrans α LE.le] (f : ι → α) (s : Finset ι) (hs : s.Nonempty) :
∃ (i : ι), MinimalFor (fun (x : ι) => x ∈ s) f i
source
theorem Finset.exists_maximal {α : Type u_2} [LE α] [IsTrans α LE.le] {s : Finset α} (hs : s.Nonempty) :
∃ (i : α), Maximal (fun (x : α) => x ∈ s) i
source
theorem Finset.exists_minimal {α : Type u_2} [LE α] [IsTrans α LE.le] {s : Finset α} (hs : s.Nonempty) :
∃ (i : α), Minimal (fun (x : α) => x ∈ s) i
source
theorem Finset.exists_le_maximal {α : Type u_2} [Preorder α] {a : α} (s : Finset α) (ha : a ∈ s) :
∃ (b : α), a ≤ b ∧ Maximal (fun (x : α) => x ∈ s) b
source
theorem Finset.exists_le_minimal {α : Type u_2} [Preorder α] {a : α} (s : Finset α) (ha : a ∈ s) :
∃ b ≤ a, Minimal (fun (x : α) => x ∈ s) b
source
@[deprecated Finset.exists_le_minimal (since := "2025-05-04")]
theorem Finset.exists_minimal_le {α : Type u_2} [Preorder α] {a : α} (s : Finset α) (ha : a ∈ s) :
∃ b ≤ a, Minimal (fun (x : α) => x ∈ s) b

Alias of `Finset.exists_le_minimal`.

source
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
source
theorem Set.Finite.exists_minimalFor {ι : Type u_1} {α : Type u_2} [LE α] [IsTrans α LE.le] (f : ι → α) (s : Set ι) (h : s.Finite) (hs : s.Nonempty) :
∃ (i : ι), MinimalFor (fun (x : ι) => x ∈ s) f i
source
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
source
theorem Set.Finite.exists_minimal {α : Type u_2} [LE α] [IsTrans α LE.le] {s : Set α} (h : s.Finite) (hs : s.Nonempty) :
∃ (i : α), Minimal (fun (x : α) => x ∈ s) i
source
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.

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

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

source
@[deprecated Set.Finite.exists_maximalFor (since := "2025-05-04")]
theorem Set.Finite.exists_maximal_wrt {ι : 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

Alias of `Set.Finite.exists_maximalFor`.

source
@[deprecated Set.Finite.exists_minimalFor (since := "2025-05-04")]
theorem Set.Finite.exists_minimal_wrt {ι : Type u_1} {α : Type u_2} [LE α] [IsTrans α LE.le] (f : ι → α) (s : Set ι) (h : s.Finite) (hs : s.Nonempty) :
∃ (i : ι), MinimalFor (fun (x : ι) => x ∈ s) f i

Alias of `Set.Finite.exists_minimalFor`.

source
@[deprecated Set.Finite.exists_maximalFor' (since := "2025-05-04")]
theorem Set.Finite.exists_maximal_wrt' {ι : 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

Alias of `Set.Finite.exists_maximalFor'`.

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

source
@[deprecated Set.Finite.exists_minimalFor' (since := "2025-05-04")]
theorem Set.Finite.exists_minimal_wrt' {ι : Type u_1} {α : Type u_2} [LE α] [IsTrans α LE.le] (f : ι → α) (s : Set ι) (h : (f '' s).Finite) (hs : s.Nonempty) :
∃ (i : ι), MinimalFor (fun (x : ι) => x ∈ s) f i

Alias of `Set.Finite.exists_minimalFor'`.

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

source
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
source
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
source
theorem Set.infinite_of_forall_exists_gt {α : Type u_2} [Preorder α] {s : Set α} [Nonempty α] (h : ∀ (a : α), ∃ b ∈ s, a < b) :
s.Infinite
source
theorem Set.infinite_of_forall_exists_lt {α : Type u_2} [Preorder α] {s : Set α} [Nonempty α] (h : ∀ (a : α), ∃ b ∈ s, b < a) :
s.Infinite
source
theorem Set.finite_isTop (α : Type u_2) [PartialOrder α] :
{a : α | IsTop a}.Finite
source
theorem Set.finite_isBot (α : Type u_2) [PartialOrder α] :
{a : α | IsBot a}.Finite
source
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
source
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
source
theorem Finite.exists_le_maximal {α : Type u_2} [Preorder α] [Finite α] {p : α → Prop} {a : α} (h : p a) :
∃ (b : α), a ≤ b ∧ Maximal p b
source
theorem Finite.exists_le_minimal {α : Type u_2} [Preorder α] [Finite α] {p : α → Prop} {a : α} (h : p a) :
∃ b ≤ a, Minimal p b