# Minimal/maximal elements of a set #

This file defines minimal and maximal of a set with respect to an arbitrary relation.

## Main declarations #

• maximals r s: Maximal elements of s with respect to r.
• minimals r s: Minimal elements of s with respect to r.

## TODO #

Do we need a Finset version?

def maximals {α : Type u_1} (r : ααProp) (s : Set α) :
Set α

Turns a set into an antichain by keeping only the "maximal" elements.

Equations
Instances For
def minimals {α : Type u_1} (r : ααProp) (s : Set α) :
Set α

Turns a set into an antichain by keeping only the "minimal" elements.

Equations
Instances For
theorem maximals_subset {α : Type u_1} (r : ααProp) (s : Set α) :
theorem minimals_subset {α : Type u_1} (r : ααProp) (s : Set α) :
@[simp]
theorem maximals_empty {α : Type u_1} (r : ααProp) :
@[simp]
theorem minimals_empty {α : Type u_1} (r : ααProp) :
@[simp]
theorem maximals_singleton {α : Type u_1} (r : ααProp) (a : α) :
maximals r {a} = {a}
@[simp]
theorem minimals_singleton {α : Type u_1} (r : ααProp) (a : α) :
minimals r {a} = {a}
theorem maximals_swap {α : Type u_1} (r : ααProp) (s : Set α) :
= minimals r s
theorem minimals_swap {α : Type u_1} (r : ααProp) (s : Set α) :
= maximals r s
theorem eq_of_mem_maximals {α : Type u_1} {r : ααProp} {s : Set α} {a : α} {b : α} [] (ha : a maximals r s) (hb : b s) (h : r a b) :
a = b
theorem eq_of_mem_minimals {α : Type u_1} {r : ααProp} {s : Set α} {a : α} {b : α} [] (ha : a minimals r s) (hb : b s) (h : r b a) :
a = b
theorem mem_maximals_iff {α : Type u_1} {r : ααProp} {s : Set α} [] {x : α} :
x maximals r s x s ∀ ⦃y : α⦄, y sr x yx = y
theorem mem_maximals_setOf_iff {α : Type u_1} {r : ααProp} [] {x : α} {P : αProp} :
x maximals r () P x ∀ ⦃y : α⦄, P yr x yx = y
theorem mem_minimals_iff {α : Type u_1} {r : ααProp} {s : Set α} [] {x : α} :
x minimals r s x s ∀ ⦃y : α⦄, y sr y xx = y
theorem mem_minimals_setOf_iff {α : Type u_1} {r : ααProp} [] {x : α} {P : αProp} :
x minimals r () P x ∀ ⦃y : α⦄, P yr y xx = y
theorem mem_minimals_iff_forall_lt_not_mem' {α : Type u_1} {r : ααProp} {s : Set α} {x : α} (rlt : ααProp) [] :
x minimals r s x s ∀ ⦃y : α⦄, rlt y xys

This theorem can't be used to rewrite without specifying rlt, since rlt would have to be guessed. See mem_minimals_iff_forall_ssubset_not_mem and mem_minimals_iff_forall_lt_not_mem for ⊆ and ≤ versions.

theorem mem_maximals_iff_forall_lt_not_mem' {α : Type u_1} {r : ααProp} {s : Set α} {x : α} (rlt : ααProp) [] :
x maximals r s x s ∀ ⦃y : α⦄, rlt x yys
theorem minimals_eq_minimals_of_subset_of_forall {α : Type u_1} {r : ααProp} {s : Set α} {t : Set α} [] [IsTrans α r] (hts : t s) (h : xs, yt, r y x) :
theorem maximals_eq_maximals_of_subset_of_forall {α : Type u_1} {r : ααProp} {s : Set α} {t : Set α} [] [IsTrans α r] (hts : t s) (h : xs, yt, r x y) :
theorem maximals_antichain {α : Type u_1} (r : ααProp) (s : Set α) [] :
theorem minimals_antichain {α : Type u_1} (r : ααProp) (s : Set α) [] :
theorem mem_minimals_iff_forall_ssubset_not_mem {α : Type u_1} {x : Set α} (s : Set (Set α)) :
x minimals (fun (x x_1 : Set α) => x x_1) s x s ∀ ⦃y : Set α⦄, y xys
theorem mem_minimals_iff_forall_lt_not_mem {α : Type u_1} {x : α} [] {s : Set α} :
x minimals (fun (x x_1 : α) => x x_1) s x s ∀ ⦃y : α⦄, y < xys
theorem mem_maximals_iff_forall_ssubset_not_mem {α : Type u_1} {x : Set α} {s : Set (Set α)} :
x maximals (fun (x x_1 : Set α) => x x_1) s x s ∀ ⦃y : Set α⦄, x yys
theorem mem_maximals_iff_forall_lt_not_mem {α : Type u_1} {x : α} [] {s : Set α} :
x maximals (fun (x x_1 : α) => x x_1) s x s ∀ ⦃y : α⦄, x < yys
theorem maximals_of_symm {α : Type u_1} (r : ααProp) (s : Set α) [IsSymm α r] :
maximals r s = s
theorem minimals_of_symm {α : Type u_1} (r : ααProp) (s : Set α) [IsSymm α r] :
minimals r s = s
theorem maximals_eq_minimals {α : Type u_1} (r : ααProp) (s : Set α) [IsSymm α r] :
theorem Set.Subsingleton.maximals_eq {α : Type u_1} {r : ααProp} {s : Set α} (h : s.Subsingleton) :
maximals r s = s
theorem Set.Subsingleton.minimals_eq {α : Type u_1} {r : ααProp} {s : Set α} (h : s.Subsingleton) :
minimals r s = s
theorem maximals_mono {α : Type u_1} {r₁ : ααProp} {r₂ : ααProp} {s : Set α} [IsAntisymm α r₂] (h : ∀ (a b : α), r₁ a br₂ a b) :
maximals r₂ s maximals r₁ s
theorem minimals_mono {α : Type u_1} {r₁ : ααProp} {r₂ : ααProp} {s : Set α} [IsAntisymm α r₂] (h : ∀ (a b : α), r₁ a br₂ a b) :
minimals r₂ s minimals r₁ s
theorem maximals_union {α : Type u_1} {r : ααProp} {s : Set α} {t : Set α} :
theorem minimals_union {α : Type u_1} {r : ααProp} {s : Set α} {t : Set α} :
theorem maximals_inter_subset {α : Type u_1} {r : ααProp} {s : Set α} {t : Set α} :
maximals r s t maximals r (s t)
theorem minimals_inter_subset {α : Type u_1} {r : ααProp} {s : Set α} {t : Set α} :
minimals r s t minimals r (s t)
theorem inter_maximals_subset {α : Type u_1} {r : ααProp} {s : Set α} {t : Set α} :
s maximals r t maximals r (s t)
theorem inter_minimals_subset {α : Type u_1} {r : ααProp} {s : Set α} {t : Set α} :
s minimals r t minimals r (s t)
theorem IsAntichain.maximals_eq {α : Type u_1} {r : ααProp} {s : Set α} (h : ) :
maximals r s = s
theorem IsAntichain.minimals_eq {α : Type u_1} {r : ααProp} {s : Set α} (h : ) :
minimals r s = s
@[simp]
theorem maximals_idem {α : Type u_1} {r : ααProp} {s : Set α} :
@[simp]
theorem minimals_idem {α : Type u_1} {r : ααProp} {s : Set α} :
theorem IsAntichain.max_maximals {α : Type u_1} {r : ααProp} {s : Set α} {t : Set α} (ht : ) (h : maximals r s t) (hs : ∀ ⦃a : α⦄, a tbmaximals r s, r b a) :
maximals r s = t

If maximals r s is included in but shadows the antichain t, then it is actually equal to t.

theorem IsAntichain.max_minimals {α : Type u_1} {r : ααProp} {s : Set α} {t : Set α} (ht : ) (h : minimals r s t) (hs : ∀ ⦃a : α⦄, a tbminimals r s, r a b) :
minimals r s = t

If minimals r s is included in but shadows the antichain t, then it is actually equal to t.

theorem IsLeast.mem_minimals {α : Type u_1} {s : Set α} {a : α} [] (h : IsLeast s a) :
a minimals (fun (x x_1 : α) => x x_1) s
theorem IsGreatest.mem_maximals {α : Type u_1} {s : Set α} {a : α} [] (h : ) :
a maximals (fun (x x_1 : α) => x x_1) s
theorem IsLeast.minimals_eq {α : Type u_1} {s : Set α} {a : α} [] (h : IsLeast s a) :
minimals (fun (x x_1 : α) => x x_1) s = {a}
theorem IsGreatest.maximals_eq {α : Type u_1} {s : Set α} {a : α} [] (h : ) :
maximals (fun (x x_1 : α) => x x_1) s = {a}
theorem IsAntichain.minimals_upperClosure {α : Type u_1} {s : Set α} [] (hs : IsAntichain (fun (x x_1 : α) => x x_1) s) :
minimals (fun (x x_1 : α) => x x_1) () = s
theorem IsAntichain.maximals_lowerClosure {α : Type u_1} {s : Set α} [] (hs : IsAntichain (fun (x x_1 : α) => x x_1) s) :
maximals (fun (x x_1 : α) => x x_1) () = s
theorem map_mem_minimals {β : Type u_2} {α : Type u_1} {f : αβ} {r : ααProp} {s : ββProp} {x : Set α} (hf : ∀ ⦃a a' : α⦄, a xa' x(r a a' s (f a) (f a'))) {a : α} (ha : a minimals r x) :
f a minimals s (f '' x)
theorem map_mem_maximals {β : Type u_2} {α : Type u_1} {f : αβ} {r : ααProp} {s : ββProp} {x : Set α} (hf : ∀ ⦃a a' : α⦄, a xa' x(r a a' s (f a) (f a'))) {a : α} (ha : a maximals r x) :
f a maximals s (f '' x)
theorem map_mem_minimals_iff {β : Type u_2} {α : Type u_1} {f : αβ} {r : ααProp} {s : ββProp} {x : Set α} (hf : ∀ ⦃a a' : α⦄, a xa' x(r a a' s (f a) (f a'))) {a : α} (ha : a x) :
f a minimals s (f '' x) a minimals r x
theorem map_mem_maximals_iff {β : Type u_2} {α : Type u_1} {f : αβ} {r : ααProp} {s : ββProp} {x : Set α} (hf : ∀ ⦃a a' : α⦄, a xa' x(r a a' s (f a) (f a'))) {a : α} (ha : a x) :
f a maximals s (f '' x) a maximals r x
theorem image_minimals_of_rel_iff_rel {β : Type u_2} {α : Type u_1} {f : αβ} {r : ααProp} {s : ββProp} {x : Set α} (hf : ∀ ⦃a a' : α⦄, a xa' x(r a a' s (f a) (f a'))) :
f '' minimals r x = minimals s (f '' x)
theorem image_maximals_of_rel_iff_rel {β : Type u_2} {α : Type u_1} {f : αβ} {r : ααProp} {s : ββProp} {x : Set α} (hf : ∀ ⦃a a' : α⦄, a xa' x(r a a' s (f a) (f a'))) :
f '' maximals r x = maximals s (f '' x)
theorem RelEmbedding.image_minimals_eq {β : Type u_2} {α : Type u_1} {r : ααProp} {s : ββProp} (f : r ↪r s) (x : Set α) :
f '' minimals r x = minimals s (f '' x)
theorem RelEmbedding.image_maximals_eq {β : Type u_2} {α : Type u_1} {r : ααProp} {s : ββProp} (f : r ↪r s) (x : Set α) :
f '' maximals r x = maximals s (f '' x)
theorem image_minimals_univ {α : Type u_1} [LE α] {s : Set α} :
Subtype.val '' minimals (fun (x x_1 : { x : α // x s }) => x x_1) Set.univ = minimals (fun (x x_1 : α) => x x_1) s
theorem image_maximals_univ {α : Type u_1} [LE α] {s : Set α} :
Subtype.val '' maximals (fun (x x_1 : { x : α // x s }) => x x_1) Set.univ = maximals (fun (x x_1 : α) => x x_1) s
theorem OrderIso.map_mem_minimals {β : Type u_2} {α : Type u_1} [LE α] [LE β] {s : Set α} {t : Set β} (f : s ≃o t) {x : α} (hx : x minimals (fun (x x_1 : α) => x x_1) s) :
(f x, ) minimals (fun (x x_1 : β) => x x_1) t
theorem OrderIso.map_mem_maximals {β : Type u_2} {α : Type u_1} [LE α] [LE β] {s : Set α} {t : Set β} (f : s ≃o t) {x : α} (hx : x maximals (fun (x x_1 : α) => x x_1) s) :
(f x, ) maximals (fun (x x_1 : β) => x x_1) t
def OrderIso.mapMinimals {β : Type u_2} {α : Type u_1} [LE α] [LE β] {s : Set α} {t : Set β} (f : s ≃o t) :
(minimals (fun (x x_1 : α) => x x_1) s) ≃o (minimals (fun (x x_1 : β) => x x_1) t)

If two sets are order isomorphic, their minimals are also order isomorphic.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def OrderIso.mapMaximals {β : Type u_2} {α : Type u_1} [LE α] [LE β] {s : Set α} {t : Set β} (f : s ≃o t) :
(maximals (fun (x x_1 : α) => x x_1) s) ≃o (maximals (fun (x x_1 : β) => x x_1) t)

If two sets are order isomorphic, their maximals are also order isomorphic.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def OrderIso.minimalsIsoMaximals {β : Type u_2} {α : Type u_1} [LE α] [LE β] {s : Set α} {t : Set β} (f : s ≃o (t)ᵒᵈ) :
(minimals (fun (x x_1 : α) => x x_1) s) ≃o ((maximals (fun (x x_1 : β) => x x_1) t))ᵒᵈ

If two sets are antitonically order isomorphic, their minimals are too.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def OrderIso.maximalsIsoMinimals {β : Type u_2} {α : Type u_1} [LE α] [LE β] {s : Set α} {t : Set β} (f : s ≃o (t)ᵒᵈ) :
(maximals (fun (x x_1 : α) => x x_1) s) ≃o ((minimals (fun (x x_1 : β) => x x_1) t))ᵒᵈ

If two sets are antitonically order isomorphic, their minimals are too.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem inter_minimals_preimage_inter_eq_of_rel_iff_rel_on {β : Type u_2} {α : Type u_1} {f : αβ} {r : ααProp} {s : ββProp} {x : Set α} (hf : ∀ ⦃a a' : α⦄, a xa' x(r a a' s (f a) (f a'))) (y : Set β) :
x f ⁻¹' minimals s (f '' x y) = minimals r (x f ⁻¹' y)
theorem inter_preimage_minimals_eq_of_rel_iff_rel_on_of_subset {β : Type u_2} {α : Type u_1} {f : αβ} {r : ααProp} {s : ββProp} {x : Set α} {y : Set β} (hf : ∀ ⦃a a' : α⦄, a xa' x(r a a' s (f a) (f a'))) (hy : y f '' x) :
x f ⁻¹' minimals s y = minimals r (x f ⁻¹' y)
theorem RelEmbedding.inter_preimage_minimals_eq {β : Type u_2} {α : Type u_1} {r : ααProp} {s : ββProp} (f : r ↪r s) (x : Set α) (y : Set β) :
x f ⁻¹' minimals s (f '' x y) = minimals r (x f ⁻¹' y)
theorem RelEmbedding.inter_preimage_minimals_eq_of_subset {β : Type u_2} {α : Type u_1} {r : ααProp} {s : ββProp} {y : Set β} {x : Set α} (f : r ↪r s) (h : y f '' x) :
x f ⁻¹' minimals s y = minimals r (x f ⁻¹' y)
theorem RelEmbedding.minimals_preimage_eq {β : Type u_2} {α : Type u_1} {r : ααProp} {s : ββProp} (f : r ↪r s) (y : Set β) :
minimals r (f ⁻¹' y) = f ⁻¹' minimals s (y )
theorem RelIso.minimals_preimage_eq {β : Type u_2} {α : Type u_1} {r : ααProp} {s : ββProp} (f : r ≃r s) (y : Set β) :
minimals r (f ⁻¹' y) = f ⁻¹' minimals s y
theorem RelIso.maximals_preimage_eq {β : Type u_2} {α : Type u_1} {r : ααProp} {s : ββProp} (f : r ≃r s) (y : Set β) :
maximals r (f ⁻¹' y) = f ⁻¹' maximals s y
theorem inter_maximals_preimage_inter_eq_of_rel_iff_rel_on {β : Type u_2} {α : Type u_1} {f : αβ} {r : ααProp} {s : ββProp} {x : Set α} (hf : ∀ ⦃a a' : α⦄, a xa' x(r a a' s (f a) (f a'))) (y : Set β) :
x f ⁻¹' maximals s (f '' x y) = maximals r (x f ⁻¹' y)
theorem inter_preimage_maximals_eq_of_rel_iff_rel_on_of_subset {β : Type u_2} {α : Type u_1} {f : αβ} {r : ααProp} {s : ββProp} {x : Set α} {y : Set β} (hf : ∀ ⦃a a' : α⦄, a xa' x(r a a' s (f a) (f a'))) (hy : y f '' x) :
x f ⁻¹' maximals s y = maximals r (x f ⁻¹' y)
theorem RelEmbedding.inter_preimage_maximals_eq {β : Type u_2} {α : Type u_1} {r : ααProp} {s : ββProp} (f : r ↪r s) (x : Set α) (y : Set β) :
x f ⁻¹' maximals s (f '' x y) = maximals r (x f ⁻¹' y)
theorem RelEmbedding.inter_preimage_maximals_eq_of_subset {β : Type u_2} {α : Type u_1} {r : ααProp} {s : ββProp} {y : Set β} {x : Set α} (f : r ↪r s) (h : y f '' x) :
x f ⁻¹' maximals s y = maximals r (x f ⁻¹' y)
theorem RelEmbedding.maximals_preimage_eq {β : Type u_2} {α : Type u_1} {r : ααProp} {s : ββProp} (f : r ↪r s) (y : Set β) :
maximals r (f ⁻¹' y) = f ⁻¹' maximals s (y )
@[simp]
theorem maximals_Iic {α : Type u_1} [] (a : α) :
maximals (fun (x x_1 : α) => x x_1) () = {a}
@[simp]
theorem minimals_Ici {α : Type u_1} [] (a : α) :
minimals (fun (x x_1 : α) => x x_1) () = {a}
theorem maximals_Icc {α : Type u_1} [] {a : α} {b : α} (hab : a b) :
maximals (fun (x x_1 : α) => x x_1) (Set.Icc a b) = {b}
theorem minimals_Icc {α : Type u_1} [] {a : α} {b : α} (hab : a b) :
minimals (fun (x x_1 : α) => x x_1) (Set.Icc a b) = {a}
theorem maximals_Ioc {α : Type u_1} [] {a : α} {b : α} (hab : a < b) :
maximals (fun (x x_1 : α) => x x_1) (Set.Ioc a b) = {b}
theorem minimals_Ico {α : Type u_1} [] {a : α} {b : α} (hab : a < b) :
minimals (fun (x x_1 : α) => x x_1) (Set.Ico a b) = {a}