mathlib 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?

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

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

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

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

Equations
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 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
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
theorem maximals_antichain {α : Type u_1} (r : α α Prop) (s : set α) [is_antisymm α r] :
theorem minimals_antichain {α : Type u_1} (r : α α Prop) (s : set α) [is_antisymm α r] :
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 α} [is_antisymm α r₂] (h : (a b : α), r₁ a b r₂ a b) :
maximals r₂ s maximals r₁ s
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
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) :