Documentation

Mathlib.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
Instances For
    def minimals {α : Type u_1} (r : ααProp) (s : Set α) :
    Set α

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

    Equations
    Instances For
      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 : α} [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 sr x yx = 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 yr x yx = y
      theorem mem_minimals_iff {α : Type u_1} {r : ααProp} {s : Set α} [IsAntisymm α r] {x : α} :
      x minimals r s x s ∀ ⦃y : α⦄, y sr y xx = 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 yr y xx = 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 xys

      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 yys
      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 : xs, ∃ y ∈ t, r y x) :
      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 : xs, ∃ y ∈ t, r x y) :
      theorem maximals_antichain {α : Type u_1} (r : ααProp) (s : Set α) [IsAntisymm α r] :
      theorem minimals_antichain {α : Type u_1} (r : ααProp) (s : Set α) [IsAntisymm α r] :
      theorem mem_minimals_iff_forall_ssubset_not_mem {α : Type u_1} {x : Set α} (s : Set (Set α)) :
      x minimals (fun (x x_1 : Set α) => x x_1) s x s ∀ ⦃y : Set α⦄, y xys
      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 < xys
      theorem mem_maximals_iff_forall_ssubset_not_mem {α : Type u_1} {x : Set α} {s : Set (Set α)} :
      x maximals (fun (x x_1 : Set α) => x x_1) s x s ∀ ⦃y : Set α⦄, x yys
      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 < yys
      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] :
      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 br₂ 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 br₂ a b) :
      minimals r₂ s minimals r₁ s
      theorem maximals_union {α : Type u_1} {r : ααProp} {s : Set α} {t : Set α} :
      theorem minimals_union {α : Type u_1} {r : ααProp} {s : Set α} {t : Set α} :
      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 α} :
      @[simp]
      theorem minimals_idem {α : Type u_1} {r : ααProp} {s : Set α} :
      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 ∈ 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 ∈ 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 map_mem_minimals {β : Type u_2} {α : Type u_1} {f : αβ} {r : ααProp} {s : ββProp} {x : Set α} (hf : ∀ ⦃a a' : α⦄, a xa' x(r a a' s (f a) (f a'))) {a : α} (ha : a minimals r x) :
      f a minimals s (f '' x)
      theorem map_mem_maximals {β : Type u_2} {α : Type u_1} {f : αβ} {r : ααProp} {s : ββProp} {x : Set α} (hf : ∀ ⦃a a' : α⦄, a xa' x(r a a' s (f a) (f a'))) {a : α} (ha : a maximals r x) :
      f a maximals s (f '' x)
      theorem map_mem_minimals_iff {β : Type u_2} {α : Type u_1} {f : αβ} {r : ααProp} {s : ββProp} {x : Set α} (hf : ∀ ⦃a a' : α⦄, a xa' x(r a a' s (f a) (f a'))) {a : α} (ha : a x) :
      f a minimals s (f '' x) a minimals r x
      theorem map_mem_maximals_iff {β : Type u_2} {α : Type u_1} {f : αβ} {r : ααProp} {s : ββProp} {x : Set α} (hf : ∀ ⦃a a' : α⦄, a xa' x(r a a' s (f a) (f a'))) {a : α} (ha : a x) :
      f a maximals s (f '' x) a maximals r x
      theorem image_minimals_of_rel_iff_rel {β : Type u_2} {α : Type u_1} {f : αβ} {r : ααProp} {s : ββProp} {x : Set α} (hf : ∀ ⦃a a' : α⦄, a xa' x(r a a' s (f a) (f a'))) :
      f '' minimals r x = minimals s (f '' x)
      theorem image_maximals_of_rel_iff_rel {β : Type u_2} {α : Type u_1} {f : αβ} {r : ααProp} {s : ββProp} {x : Set α} (hf : ∀ ⦃a a' : α⦄, a xa' x(r a a' s (f a) (f a'))) :
      f '' maximals r x = maximals s (f '' x)
      theorem RelEmbedding.image_minimals_eq {β : Type u_2} {α : Type u_1} {r : ααProp} {s : ββProp} (f : r ↪r s) (x : Set α) :
      f '' minimals r x = minimals s (f '' x)
      theorem RelEmbedding.image_maximals_eq {β : Type u_2} {α : Type u_1} {r : ααProp} {s : ββProp} (f : r ↪r s) (x : Set α) :
      f '' maximals r x = maximals s (f '' x)
      theorem image_minimals_univ {α : Type u_1} [LE α] {s : Set α} :
      Subtype.val '' minimals (fun (x x_1 : { x : α // x s }) => x x_1) Set.univ = minimals (fun (x x_1 : α) => x x_1) s
      theorem image_maximals_univ {α : Type u_1} [LE α] {s : Set α} :
      Subtype.val '' maximals (fun (x x_1 : { x : α // x s }) => x x_1) Set.univ = maximals (fun (x x_1 : α) => x x_1) s
      theorem OrderIso.map_mem_minimals {β : Type u_2} {α : Type u_1} [LE α] [LE β] {s : Set α} {t : Set β} (f : s ≃o t) {x : α} (hx : x minimals (fun (x x_1 : α) => x x_1) s) :
      (f { val := x, property := (_ : x s) }) minimals (fun (x x_1 : β) => x x_1) t
      theorem OrderIso.map_mem_maximals {β : Type u_2} {α : Type u_1} [LE α] [LE β] {s : Set α} {t : Set β} (f : s ≃o t) {x : α} (hx : x maximals (fun (x x_1 : α) => x x_1) s) :
      (f { val := x, property := (_ : x s) }) maximals (fun (x x_1 : β) => x x_1) t
      def OrderIso.mapMinimals {β : Type u_2} {α : Type u_1} [LE α] [LE β] {s : Set α} {t : Set β} (f : s ≃o t) :
      (minimals (fun (x x_1 : α) => x x_1) s) ≃o (minimals (fun (x x_1 : β) => x x_1) t)

      If two sets are order isomorphic, their minimals are also order isomorphic.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def OrderIso.mapMaximals {β : Type u_2} {α : Type u_1} [LE α] [LE β] {s : Set α} {t : Set β} (f : s ≃o t) :
        (maximals (fun (x x_1 : α) => x x_1) s) ≃o (maximals (fun (x x_1 : β) => x x_1) t)

        If two sets are order isomorphic, their maximals are also order isomorphic.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def OrderIso.minimalsIsoMaximals {β : Type u_2} {α : Type u_1} [LE α] [LE β] {s : Set α} {t : Set β} (f : s ≃o (t)ᵒᵈ) :
          (minimals (fun (x x_1 : α) => x x_1) s) ≃o ((maximals (fun (x x_1 : β) => x x_1) t))ᵒᵈ

          If two sets are antitonically order isomorphic, their minimals are too.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def OrderIso.maximalsIsoMinimals {β : Type u_2} {α : Type u_1} [LE α] [LE β] {s : Set α} {t : Set β} (f : s ≃o (t)ᵒᵈ) :
            (maximals (fun (x x_1 : α) => x x_1) s) ≃o ((minimals (fun (x x_1 : β) => x x_1) t))ᵒᵈ

            If two sets are antitonically order isomorphic, their minimals are too.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              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 xa' 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 xa' 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 xa' 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 xa' 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}