mathlib documentation

order.minimal

Minimal/maximal elements of a set #

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

Main declarations #

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 ∈ s | ∀ ⦃b : α⦄, b sr a ba = b}
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 ∈ s | ∀ ⦃b : α⦄, b sr b aa = b}
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 α) :
theorem minimals_swap {α : Type u_1} (r : α → α → Prop) (s : set α) :
theorem maximals_antichain {α : Type u_1} (r : α → α → Prop) (s : set α) :
theorem minimals_antichain {α : Type u_1} (r : α → α → Prop) (s : set α) :
theorem maximals_eq_minimals {α : Type u_1} (r : α → α → Prop) (s : set α) [is_symm α 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₁ r₂ : α → α → Prop} {s : set α} (h : ∀ (a b : α), r₁ a br₂ a b) :
maximals r₂ s maximals r₁ s
theorem minimals_mono {α : Type u_1} {r₁ r₂ : α → α → Prop} {s : set α} (h : ∀ (a b : α), r₁ a br₂ a b) :
minimals r₂ s minimals r₁ s
theorem maximals_union {α : Type u_1} {r : α → α → Prop} {s t : set α} :
theorem minimals_union {α : Type u_1} {r : α → α → Prop} {s t : set α} :
theorem maximals_inter_subset {α : Type u_1} {r : α → α → Prop} {s t : set α} :
maximals r s t maximals r (s t)
theorem minimals_inter_subset {α : Type u_1} {r : α → α → Prop} {s t : set α} :
minimals r s t minimals r (s t)
theorem inter_maximals_subset {α : Type u_1} {r : α → α → Prop} {s t : set α} :
s maximals r t maximals r (s t)
theorem inter_minimals_subset {α : Type u_1} {r : α → α → Prop} {s t : set α} :
s minimals r t minimals r (s t)
theorem is_antichain.maximals_eq {α : Type u_1} {r : α → α → Prop} {s : set α} (h : is_antichain r s) :
maximals r s = s
theorem is_antichain.minimals_eq {α : Type u_1} {r : α → α → Prop} {s : set α} (h : is_antichain r s) :
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 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.

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.

theorem is_least.mem_minimals {α : Type u_1} {s : set α} {a : α} [partial_order α] (h : is_least s a) :
theorem is_greatest.mem_maximals {α : Type u_1} {s : set α} {a : α} [partial_order α] (h : is_greatest s a) :
theorem is_least.minimals_eq {α : Type u_1} {s : set α} {a : α} [partial_order α] (h : is_least s a) :
theorem is_greatest.maximals_eq {α : Type u_1} {s : set α} {a : α} [partial_order α] (h : is_greatest s a) :