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 : α), x ∈ s → ∃ y, 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 : α), x ∈ s → ∃ y, 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 => 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 => 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 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 : Set.Subsingleton s) : maximals r s = s

theorem Set.Subsingleton.minimals_eq {α : Type u_1} {r : α → α → Prop} {s : Set α} (h : Set.Subsingleton s) : 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, 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, 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 minimals_image_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'))) : minimals s (f '' x) = f '' minimals r x

theorem maximals_image_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'))) : maximals s (f '' x) = f '' maximals r x

theorem RelEmbedding.minimals_image_eq {β : Type u_2} {α : Type u_1} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) (x : Set α) : minimals s (↑f '' x) = ↑f '' minimals r x

theorem RelEmbedding.maximals_image_eq {β : Type u_2} {α : Type u_1} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) (x : Set α) : maximals s (↑f '' x) = ↑f '' maximals r x

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 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}