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 #
maximals r s
: Maximal elements ofs
with respect tor
.minimals r s
: Minimal elements ofs
with respect tor
.
TODO #
Do we need a finset
version?
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
maximals_antichain
{α : Type u_1}
(r : α → α → Prop)
(s : set α)
[is_antisymm α r] :
is_antichain r (maximals r s)
theorem
minimals_antichain
{α : Type u_1}
(r : α → α → Prop)
(s : set α)
[is_antisymm α r] :
is_antichain r (minimals r s)
theorem
set.subsingleton.maximals_eq
{α : Type u_1}
{r : α → α → Prop}
{s : set α}
(h : s.subsingleton) :
theorem
set.subsingleton.minimals_eq
{α : Type u_1}
{r : α → α → Prop}
{s : set α}
(h : s.subsingleton) :
theorem
is_antichain.maximals_eq
{α : Type u_1}
{r : α → α → Prop}
{s : set α}
(h : is_antichain r s) :
theorem
is_antichain.minimals_eq
{α : Type u_1}
{r : α → α → Prop}
{s : set α}
(h : is_antichain r s) :
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) :
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
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