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.
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 α LE.le]
(f : ι → α)
(s : Finset ι)
(hs : s.Nonempty)
:
∃ (i : ι), MinimalFor (fun (x : ι) => x ∈ s) f i
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 α LE.le]
(f : ι → α)
(s : Set ι)
(h : s.Finite)
(hs : s.Nonempty)
:
∃ (i : ι), MinimalFor (fun (x : ι) => x ∈ s) f 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 α 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.
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.