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

• maximals r s = {a : α | a ∈ s ∧ ∀ ⦃b : α⦄, b ∈ s → r a b → r b a}

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

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

Equations

• minimals r s = {a : α | a ∈ s ∧ ∀ ⦃b : α⦄, b ∈ s → r b a → r a b}

theorem maximals_subset {α : Type u_1} (r : α → α → Prop) (s : Set α) : maximals r s ⊆ s

theorem minimals_subset {α : Type u_1} (r : α → α → Prop) (s : Set α) : minimals r s ⊆ s

@[simp]

theorem maximals_empty {α : Type u_1} (r : α → α → Prop) : maximals r ∅ = ∅

@[simp]

theorem minimals_empty {α : Type u_1} (r : α → α → Prop) : minimals r ∅ = ∅

@[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 α) : maximals (Function.swap r) s = minimals r s

theorem minimals_swap {α : Type u_1} (r : α → α → Prop) (s : Set α) : minimals (Function.swap r) s = maximals r s

theorem eq_of_mem_maximals {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α} {b : α} [IsAntisymm α r] (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 : α} [IsAntisymm α r] (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 α} [IsAntisymm α r] {x : α} : x ∈ maximals r s ↔ x ∈ s ∧ ∀ ⦃y : α⦄, y ∈ s → r x y → x = y

theorem mem_maximals_setOf_iff {α : Type u_1} {r : α → α → Prop} [IsAntisymm α r] {x : α} {P : α → Prop} : x ∈ maximals r (setOf P) ↔ P x ∧ ∀ ⦃y : α⦄, P y → r x y → x = y

theorem mem_minimals_iff {α : Type u_1} {r : α → α → Prop} {s : Set α} [IsAntisymm α r] {x : α} : x ∈ minimals r s ↔ x ∈ s ∧ ∀ ⦃y : α⦄, y ∈ s → r y x → x = y

theorem mem_minimals_setOf_iff {α : Type u_1} {r : α → α → Prop} [IsAntisymm α r] {x : α} {P : α → Prop} : x ∈ minimals r (setOf P) ↔ P x ∧ ∀ ⦃y : α⦄, P y → r y x → x = y

theorem mem_minimals_iff_forall_lt_not_mem' {α : Type u_1} {r : α → α → Prop} {s : Set α} {x : α} (rlt : α → α → Prop) [IsNonstrictStrictOrder α r rlt] : x ∈ minimals r s ↔ x ∈ s ∧ ∀ ⦃y : α⦄, rlt y x → y ∉ s

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) [IsNonstrictStrictOrder α r rlt] : x ∈ maximals r s ↔ x ∈ s ∧ ∀ ⦃y : α⦄, rlt x y → y ∉ s

theorem minimals_eq_minimals_of_subset_of_forall {α : Type u_1} {r : α → α → Prop} {s : Set α} {t : Set α} [IsAntisymm α r] [IsTrans α r] (hts : t ⊆ s) (h : ∀ x ∈ s, ∃ y ∈ t, r y x) : minimals r s = minimals r t

theorem maximals_eq_maximals_of_subset_of_forall {α : Type u_1} {r : α → α → Prop} {s : Set α} {t : Set α} [IsAntisymm α r] [IsTrans α r] (hts : t ⊆ s) (h : ∀ x ∈ s, ∃ y ∈ t, r x y) : maximals r s = maximals r t

theorem maximals_antichain {α : Type u_1} (r : α → α → Prop) (s : Set α) [IsAntisymm α r] : IsAntichain r (maximals r s)

theorem minimals_antichain {α : Type u_1} (r : α → α → Prop) (s : Set α) [IsAntisymm α r] : IsAntichain r (minimals r s)

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 ⊂ x → y ∉ s

theorem mem_minimals_iff_forall_lt_not_mem {α : Type u_1} {x : α} [PartialOrder α] {s : Set α} : x ∈ minimals (fun (x x_1 : α) => x ≤ x_1) s ↔ x ∈ s ∧ ∀ ⦃y : α⦄, y < x → y ∉ s

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 ⊂ y → y ∉ s

theorem mem_maximals_iff_forall_lt_not_mem {α : Type u_1} {x : α} [PartialOrder α] {s : Set α} : x ∈ maximals (fun (x x_1 : α) => x ≤ x_1) s ↔ x ∈ s ∧ ∀ ⦃y : α⦄, x < y → y ∉ s

theorem Set.mem_maximals_iff_forall_insert {α : Type u_1} (s : Set α) {P : Set α → Prop} (hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s) : s ∈ maximals (fun (x x_1 : Set α) => x ⊆ x_1) {t : Set α | P t} ↔ P s ∧ ∀ x ∉ s, ¬P (insert x s)

theorem Set.mem_minimals_iff_forall_diff_singleton {α : Type u_1} (s : Set α) {P : Set α → Prop} (hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t) : s ∈ minimals (fun (x x_1 : Set α) => x ⊆ x_1) {t : Set α | P t} ↔ P s ∧ ∀ x ∈ s, ¬P (s \ {x})

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] : maximals r s = minimals r s

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 b → r₂ 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 b → r₂ a b) : minimals r₂ s ⊆ minimals r₁ s

theorem maximals_union {α : Type u_1} {r : α → α → Prop} {s : Set α} {t : Set α} : maximals r (s ∪ t) ⊆ maximals r s ∪ maximals r t

theorem minimals_union {α : Type u_1} {r : α → α → Prop} {s : Set α} {t : Set α} : minimals r (s ∪ t) ⊆ minimals r s ∪ minimals r t

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 : IsAntichain r s) : maximals r s = s

theorem IsAntichain.minimals_eq {α : Type u_1} {r : α → α → Prop} {s : Set α} (h : IsAntichain r s) : minimals r s = s

@[simp]

theorem maximals_idem {α : Type u_1} {r : α → α → Prop} {s : Set α} : maximals r (maximals r s) = maximals r s

@[simp]

theorem minimals_idem {α : Type u_1} {r : α → α → Prop} {s : Set α} : minimals r (minimals r s) = minimals r s

theorem IsAntichain.max_maximals {α : Type u_1} {r : α → α → Prop} {s : Set α} {t : Set α} (ht : IsAntichain r t) (h : maximals r s ⊆ t) (hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b ∈ maximals 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 : IsAntichain r t) (h : minimals r s ⊆ t) (hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b ∈ minimals 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 : α} [PartialOrder α] (h : IsLeast s a) : a ∈ minimals (fun (x x_1 : α) => x ≤ x_1) s

theorem IsGreatest.mem_maximals {α : Type u_1} {s : Set α} {a : α} [PartialOrder α] (h : IsGreatest s a) : a ∈ maximals (fun (x x_1 : α) => x ≤ x_1) s

theorem IsLeast.minimals_eq {α : Type u_1} {s : Set α} {a : α} [PartialOrder α] (h : IsLeast s a) : minimals (fun (x x_1 : α) => x ≤ x_1) s = {a}

theorem IsGreatest.maximals_eq {α : Type u_1} {s : Set α} {a : α} [PartialOrder α] (h : IsGreatest s a) : maximals (fun (x x_1 : α) => x ≤ x_1) s = {a}

theorem IsAntichain.minimals_upperClosure {α : Type u_1} {s : Set α} [PartialOrder α] (hs : IsAntichain (fun (x x_1 : α) => x ≤ x_1) s) : minimals (fun (x x_1 : α) => x ≤ x_1) ↑(upperClosure s) = s

theorem IsAntichain.maximals_lowerClosure {α : Type u_1} {s : Set α} [PartialOrder α] (hs : IsAntichain (fun (x x_1 : α) => x ≤ x_1) s) : maximals (fun (x x_1 : α) => x ≤ x_1) ↑(lowerClosure s) = s

theorem map_mem_minimals {β : Type u_2} {α : Type u_1} {f : α → β} {r : α → α → Prop} {s : β → β → Prop} {x : Set α} (hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ 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 ∈ x → a' ∈ 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 ∈ x → a' ∈ 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 ∈ x → a' ∈ 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 ∈ x → a' ∈ 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 ∈ x → a' ∈ 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.

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.

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.

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.

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 ∈ x → a' ∈ 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 ∈ x → a' ∈ 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 ∩ Set.range ⇑f)

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 ∈ x → a' ∈ 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 ∈ x → a' ∈ 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 ∩ Set.range ⇑f)

@[simp]

theorem maximals_Iic {α : Type u_1} [PartialOrder α] (a : α) : maximals (fun (x x_1 : α) => x ≤ x_1) (Set.Iic a) = {a}

@[simp]

theorem minimals_Ici {α : Type u_1} [PartialOrder α] (a : α) : minimals (fun (x x_1 : α) => x ≤ x_1) (Set.Ici a) = {a}

theorem maximals_Icc {α : Type u_1} [PartialOrder α] {a : α} {b : α} (hab : a ≤ b) : maximals (fun (x x_1 : α) => x ≤ x_1) (Set.Icc a b) = {b}

theorem minimals_Icc {α : Type u_1} [PartialOrder α] {a : α} {b : α} (hab : a ≤ b) : minimals (fun (x x_1 : α) => x ≤ x_1) (Set.Icc a b) = {a}

theorem maximals_Ioc {α : Type u_1} [PartialOrder α] {a : α} {b : α} (hab : a < b) : maximals (fun (x x_1 : α) => x ≤ x_1) (Set.Ioc a b) = {b}

theorem minimals_Ico {α : Type u_1} [PartialOrder α] {a : α} {b : α} (hab : a < b) : minimals (fun (x x_1 : α) => x ≤ x_1) (Set.Ico a b) = {a}