mathlib3 documentation

order.minimal

Minimal/maximal elements of a set #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main declarations #

TODO #

Do we need a finset version?

source
def maximals {α : Type u_1} (r : α → α → Prop) (s : set α) :
set α

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

Equations
source
def minimals {α : Type u_1} (r : α → α → Prop) (s : set α) :
set α

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

Equations
source
theorem maximals_subset {α : Type u_1} (r : α → α → Prop) (s : set α) :
maximals r s ⊆ s
source
theorem minimals_subset {α : Type u_1} (r : α → α → Prop) (s : set α) :
minimals r s ⊆ s
source
@[simp]
theorem maximals_empty {α : Type u_1} (r : α → α → Prop) :
maximals r ∅ = ∅
source
@[simp]
theorem minimals_empty {α : Type u_1} (r : α → α → Prop) :
minimals r ∅ = ∅
source
@[simp]
theorem maximals_singleton {α : Type u_1} (r : α → α → Prop) (a : α) :
maximals r {a} = {a}
source
@[simp]
theorem minimals_singleton {α : Type u_1} (r : α → α → Prop) (a : α) :
minimals r {a} = {a}
source
theorem maximals_swap {α : Type u_1} (r : α → α → Prop) (s : set α) :
maximals (function.swap r) s = minimals r s
source
theorem minimals_swap {α : Type u_1} (r : α → α → Prop) (s : set α) :
minimals (function.swap r) s = maximals r s
source
theorem eq_of_mem_maximals {α : Type u_1} {r : α → α → Prop} {s : set α} {a b : α} [is_antisymm α r] (ha : a ∈ maximals r s) (hb : b ∈ s) (h : r a b) :
a = b
source
theorem eq_of_mem_minimals {α : Type u_1} {r : α → α → Prop} {s : set α} {a b : α} [is_antisymm α r] (ha : a ∈ minimals r s) (hb : b ∈ s) (h : r b a) :
a = b
source
theorem maximals_antichain {α : Type u_1} (r : α → α → Prop) (s : set α) [is_antisymm α r] :
is_antichain r (maximals r s)
source
theorem minimals_antichain {α : Type u_1} (r : α → α → Prop) (s : set α) [is_antisymm α r] :
is_antichain r (minimals r s)
source
theorem maximals_eq_minimals {α : Type u_1} (r : α → α → Prop) (s : set α) [is_symm α r] :
maximals r s = minimals r s
source
theorem set.subsingleton.maximals_eq {α : Type u_1} {r : α → α → Prop} {s : set α} (h : s.subsingleton) :
maximals r s = s
source
theorem set.subsingleton.minimals_eq {α : Type u_1} {r : α → α → Prop} {s : set α} (h : s.subsingleton) :
minimals r s = s
source
theorem maximals_mono {α : Type u_1} {r₁ r₂ : α → α → Prop} {s : set α} [is_antisymm α r₂] (h : ∀ (a b : α), r₁ a b → r₂ a b) :
maximals r₂ s ⊆ maximals r₁ s
source
theorem minimals_mono {α : Type u_1} {r₁ r₂ : α → α → Prop} {s : set α} [is_antisymm α r₂] (h : ∀ (a b : α), r₁ a b → r₂ a b) :
minimals r₂ s ⊆ minimals r₁ s
source
theorem maximals_union {α : Type u_1} {r : α → α → Prop} {s t : set α} :
maximals r (s ∪ t) ⊆ maximals r s ∪ maximals r t
source
theorem minimals_union {α : Type u_1} {r : α → α → Prop} {s t : set α} :
minimals r (s ∪ t) ⊆ minimals r s ∪ minimals r t
source
theorem maximals_inter_subset {α : Type u_1} {r : α → α → Prop} {s t : set α} :
maximals r s ∩ t ⊆ maximals r (s ∩ t)
source
theorem minimals_inter_subset {α : Type u_1} {r : α → α → Prop} {s t : set α} :
minimals r s ∩ t ⊆ minimals r (s ∩ t)
source
theorem inter_maximals_subset {α : Type u_1} {r : α → α → Prop} {s t : set α} :
s ∩ maximals r t ⊆ maximals r (s ∩ t)
source
theorem inter_minimals_subset {α : Type u_1} {r : α → α → Prop} {s t : set α} :
s ∩ minimals r t ⊆ minimals r (s ∩ t)
source
theorem is_antichain.maximals_eq {α : Type u_1} {r : α → α → Prop} {s : set α} (h : is_antichain r s) :
maximals r s = s
source
theorem is_antichain.minimals_eq {α : Type u_1} {r : α → α → Prop} {s : set α} (h : is_antichain r s) :
minimals r s = s
source
@[simp]
theorem maximals_idem {α : Type u_1} {r : α → α → Prop} {s : set α} :
maximals r (maximals r s) = maximals r s
source
@[simp]
theorem minimals_idem {α : Type u_1} {r : α → α → Prop} {s : set α} :
minimals r (minimals r s) = minimals r s
source
theorem is_antichain.max_maximals {α : Type u_1} {r : α → α → Prop} {s t : set α} (ht : is_antichain r t) (h : maximals r s ⊆ t) (hs : ∀ ⦃a : α⦄, a ∈ t → (∃ (b : α) (H : 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.

source
theorem is_antichain.max_minimals {α : Type u_1} {r : α → α → Prop} {s t : set α} (ht : is_antichain r t) (h : minimals r s ⊆ t) (hs : ∀ ⦃a : α⦄, a ∈ t → (∃ (b : α) (H : 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.

source
theorem is_least.mem_minimals {α : Type u_1} {s : set α} {a : α} [partial_order α] (h : is_least s a) :
a ∈ minimals has_le.le s
source
theorem is_greatest.mem_maximals {α : Type u_1} {s : set α} {a : α} [partial_order α] (h : is_greatest s a) :
a ∈ maximals has_le.le s
source
theorem is_least.minimals_eq {α : Type u_1} {s : set α} {a : α} [partial_order α] (h : is_least s a) :
minimals has_le.le s = {a}
source
theorem is_greatest.maximals_eq {α : Type u_1} {s : set α} {a : α} [partial_order α] (h : is_greatest s a) :
maximals has_le.le s = {a}
source
theorem is_antichain.minimals_upper_closure {α : Type u_1} {s : set α} [partial_order α] (hs : is_antichain has_le.le s) :
minimals has_le.le ↑(upper_closure s) = s
source
theorem is_antichain.maximals_lower_closure {α : Type u_1} {s : set α} [partial_order α] (hs : is_antichain has_le.le s) :
maximals has_le.le ↑(lower_closure s) = s