Documentation

Mathlib.Order.Minimal

Minimality and Maximality #

This file defines minimality and maximality of an element with respect to a predicate P on an ordered type α.

Main declarations #

Implementation Details #

This file underwent a refactor from a version where minimality and maximality were defined using sets rather than predicates, and with an unbundled order relation rather than a LE instance.

A side effect is that it has become less straightforward to state that something is minimal with respect to a relation that is not defeq to the default LE. One possible way would be with a type synonym, and another would be with an ad hoc LE instance and @ notation. This was not an issue in practice anywhere in mathlib at the time of the refactor, but it may be worth re-examining this to make it easier in the future; see the TODO below.

TODO #

def Minimal {α : Type u_1} [LE α] (P : αProp) (x : α) :

Minimal P x means that x is a minimal element satisfying P.

Equations
Instances For
    def Maximal {α : Type u_1} [LE α] (P : αProp) (x : α) :

    Maximal P x means that x is a maximal element satisfying P.

    Equations
    Instances For
      theorem Minimal.prop {α : Type u_1} {P : αProp} {x : α} [LE α] (h : Minimal P x) :
      P x
      theorem Maximal.prop {α : Type u_1} {P : αProp} {x : α} [LE α] (h : Maximal P x) :
      P x
      theorem Minimal.le_of_le {α : Type u_1} {P : αProp} {x : α} {y : α} [LE α] (h : Minimal P x) (hy : P y) (hle : y x) :
      x y
      theorem Maximal.le_of_ge {α : Type u_1} {P : αProp} {x : α} {y : α} [LE α] (h : Maximal P x) (hy : P y) (hge : x y) :
      y x
      @[simp]
      theorem minimal_toDual {α : Type u_1} {P : αProp} {x : α} [LE α] :
      Minimal (fun (x : αᵒᵈ) => P (OrderDual.ofDual x)) (OrderDual.toDual x) Maximal P x
      theorem Minimal.dual {α : Type u_1} {P : αProp} {x : α} [LE α] :
      Maximal P xMinimal (fun (x : αᵒᵈ) => P (OrderDual.ofDual x)) (OrderDual.toDual x)

      Alias of the reverse direction of minimal_toDual.

      theorem Minimal.of_dual {α : Type u_1} {P : αProp} {x : α} [LE α] :
      Minimal (fun (x : αᵒᵈ) => P (OrderDual.ofDual x)) (OrderDual.toDual x)Maximal P x

      Alias of the forward direction of minimal_toDual.

      @[simp]
      theorem maximal_toDual {α : Type u_1} {P : αProp} {x : α} [LE α] :
      Maximal (fun (x : αᵒᵈ) => P (OrderDual.ofDual x)) (OrderDual.toDual x) Minimal P x
      theorem Maximal.dual {α : Type u_1} {P : αProp} {x : α} [LE α] :
      Minimal P xMaximal (fun (x : αᵒᵈ) => P (OrderDual.ofDual x)) (OrderDual.toDual x)

      Alias of the reverse direction of maximal_toDual.

      theorem Maximal.of_dual {α : Type u_1} {P : αProp} {x : α} [LE α] :
      Maximal (fun (x : αᵒᵈ) => P (OrderDual.ofDual x)) (OrderDual.toDual x)Minimal P x

      Alias of the forward direction of maximal_toDual.

      @[simp]
      theorem minimal_false {α : Type u_1} {x : α} [LE α] :
      ¬Minimal (fun (x : α) => False) x
      @[simp]
      theorem maximal_false {α : Type u_1} {x : α} [LE α] :
      ¬Maximal (fun (x : α) => False) x
      @[simp]
      theorem minimal_true {α : Type u_1} {x : α} [LE α] :
      Minimal (fun (x : α) => True) x IsMin x
      @[simp]
      theorem maximal_true {α : Type u_1} {x : α} [LE α] :
      Maximal (fun (x : α) => True) x IsMax x
      @[simp]
      theorem minimal_subtype {α : Type u_1} {P : αProp} {Q : αProp} [LE α] {x : Subtype Q} :
      Minimal (fun (x : Subtype Q) => P x) x Minimal (P Q) x
      @[simp]
      theorem maximal_subtype {α : Type u_1} {P : αProp} {Q : αProp} [LE α] {x : Subtype Q} :
      Maximal (fun (x : Subtype Q) => P x) x Maximal (P Q) x
      theorem maximal_true_subtype {α : Type u_1} {P : αProp} [LE α] {x : Subtype P} :
      Maximal (fun (x : Subtype P) => True) x Maximal P x
      theorem minimal_true_subtype {α : Type u_1} {P : αProp} [LE α] {x : Subtype P} :
      Minimal (fun (x : Subtype P) => True) x Minimal P x
      @[simp]
      theorem minimal_minimal {α : Type u_1} {P : αProp} {x : α} [LE α] :
      @[simp]
      theorem maximal_maximal {α : Type u_1} {P : αProp} {x : α} [LE α] :
      theorem minimal_iff_isMin {α : Type u_1} {P : αProp} {x : α} [LE α] (hP : ∀ ⦃x y : α⦄, P yx yP x) :
      Minimal P x P x IsMin x

      If P is down-closed, then minimal elements satisfying P are exactly the globally minimal elements satisfying P.

      theorem maximal_iff_isMax {α : Type u_1} {P : αProp} {x : α} [LE α] (hP : ∀ ⦃x y : α⦄, P yy xP x) :
      Maximal P x P x IsMax x

      If P is up-closed, then maximal elements satisfying P are exactly the globally maximal elements satisfying P.

      theorem Minimal.mono {α : Type u_1} {P : αProp} {Q : αProp} {x : α} [LE α] (h : Minimal P x) (hle : Q P) (hQ : Q x) :
      theorem Maximal.mono {α : Type u_1} {P : αProp} {Q : αProp} {x : α} [LE α] (h : Maximal P x) (hle : Q P) (hQ : Q x) :
      theorem Minimal.and_right {α : Type u_1} {P : αProp} {Q : αProp} {x : α} [LE α] (h : Minimal P x) (hQ : Q x) :
      Minimal (fun (x : α) => P x Q x) x
      theorem Minimal.and_left {α : Type u_1} {P : αProp} {Q : αProp} {x : α} [LE α] (h : Minimal P x) (hQ : Q x) :
      Minimal (fun (x : α) => Q x P x) x
      theorem Maximal.and_right {α : Type u_1} {P : αProp} {Q : αProp} {x : α} [LE α] (h : Maximal P x) (hQ : Q x) :
      Maximal (fun (x : α) => P x Q x) x
      theorem Maximal.and_left {α : Type u_1} {P : αProp} {Q : αProp} {x : α} [LE α] (h : Maximal P x) (hQ : Q x) :
      Maximal (fun (x : α) => Q x P x) x
      @[simp]
      theorem minimal_eq_iff {α : Type u_1} {x : α} {y : α} [LE α] :
      Minimal (fun (x : α) => x = y) x x = y
      @[simp]
      theorem maximal_eq_iff {α : Type u_1} {x : α} {y : α} [LE α] :
      Maximal (fun (x : α) => x = y) x x = y
      theorem not_minimal_iff {α : Type u_1} {P : αProp} {x : α} [LE α] (hx : P x) :
      ¬Minimal P x ∃ (y : α), P y y x ¬x y
      theorem not_maximal_iff {α : Type u_1} {P : αProp} {x : α} [LE α] (hx : P x) :
      ¬Maximal P x ∃ (y : α), P y x y ¬y x
      theorem Minimal.or {α : Type u_1} {P : αProp} {Q : αProp} {x : α} [LE α] (h : Minimal (fun (x : α) => P x Q x) x) :
      theorem Maximal.or {α : Type u_1} {P : αProp} {Q : αProp} {x : α} [LE α] (h : Maximal (fun (x : α) => P x Q x) x) :
      theorem minimal_and_iff_right_of_imp {α : Type u_1} {P : αProp} {Q : αProp} {x : α} [LE α] (hPQ : ∀ ⦃x : α⦄, P xQ x) :
      Minimal (fun (x : α) => P x Q x) x Minimal P x Q x
      theorem minimal_and_iff_left_of_imp {α : Type u_1} {P : αProp} {Q : αProp} {x : α} [LE α] (hPQ : ∀ ⦃x : α⦄, P xQ x) :
      Minimal (fun (x : α) => Q x P x) x Q x Minimal P x
      theorem maximal_and_iff_right_of_imp {α : Type u_1} {P : αProp} {Q : αProp} {x : α} [LE α] (hPQ : ∀ ⦃x : α⦄, P xQ x) :
      Maximal (fun (x : α) => P x Q x) x Maximal P x Q x
      theorem maximal_and_iff_left_of_imp {α : Type u_1} {P : αProp} {Q : αProp} {x : α} [LE α] (hPQ : ∀ ⦃x : α⦄, P xQ x) :
      Maximal (fun (x : α) => Q x P x) x Q x Maximal P x
      theorem minimal_iff_forall_lt {α : Type u_1} {P : αProp} {x : α} [Preorder α] :
      Minimal P x P x ∀ ⦃y : α⦄, y < x¬P y
      theorem maximal_iff_forall_gt {α : Type u_1} {P : αProp} {x : α} [Preorder α] :
      Maximal P x P x ∀ ⦃y : α⦄, x < y¬P y
      theorem Minimal.not_prop_of_lt {α : Type u_1} {P : αProp} {x : α} {y : α} [Preorder α] (h : Minimal P x) (hlt : y < x) :
      ¬P y
      theorem Maximal.not_prop_of_gt {α : Type u_1} {P : αProp} {x : α} {y : α} [Preorder α] (h : Maximal P x) (hlt : x < y) :
      ¬P y
      theorem Minimal.not_lt {α : Type u_1} {P : αProp} {x : α} {y : α} [Preorder α] (h : Minimal P x) (hy : P y) :
      ¬y < x
      theorem Maximal.not_gt {α : Type u_1} {P : αProp} {x : α} {y : α} [Preorder α] (h : Maximal P x) (hy : P y) :
      ¬x < y
      @[simp]
      theorem minimal_le_iff {α : Type u_1} {x : α} {y : α} [Preorder α] :
      Minimal (fun (x : α) => x y) x x y IsMin x
      @[simp]
      theorem maximal_ge_iff {α : Type u_1} {x : α} {y : α} [Preorder α] :
      Maximal (fun (x : α) => y x) x y x IsMax x
      @[simp]
      theorem minimal_lt_iff {α : Type u_1} {x : α} {y : α} [Preorder α] :
      Minimal (fun (x : α) => x < y) x x < y IsMin x
      @[simp]
      theorem maximal_gt_iff {α : Type u_1} {x : α} {y : α} [Preorder α] :
      Maximal (fun (x : α) => y < x) x y < x IsMax x
      theorem not_minimal_iff_exists_lt {α : Type u_1} {P : αProp} {x : α} [Preorder α] (hx : P x) :
      ¬Minimal P x y < x, P y
      theorem exists_lt_of_not_minimal {α : Type u_1} {P : αProp} {x : α} [Preorder α] (hx : P x) :
      ¬Minimal P xy < x, P y

      Alias of the forward direction of not_minimal_iff_exists_lt.

      theorem not_maximal_iff_exists_gt {α : Type u_1} {P : αProp} {x : α} [Preorder α] (hx : P x) :
      ¬Maximal P x ∃ (y : α), x < y P y
      theorem exists_gt_of_not_maximal {α : Type u_1} {P : αProp} {x : α} [Preorder α] (hx : P x) :
      ¬Maximal P x∃ (y : α), x < y P y

      Alias of the forward direction of not_maximal_iff_exists_gt.

      theorem Minimal.eq_of_ge {α : Type u_1} {P : αProp} {x : α} {y : α} [PartialOrder α] (hx : Minimal P x) (hy : P y) (hge : y x) :
      x = y
      theorem Minimal.eq_of_le {α : Type u_1} {P : αProp} {x : α} {y : α} [PartialOrder α] (hx : Minimal P x) (hy : P y) (hle : y x) :
      y = x
      theorem Maximal.eq_of_le {α : Type u_1} {P : αProp} {x : α} {y : α} [PartialOrder α] (hx : Maximal P x) (hy : P y) (hle : x y) :
      x = y
      theorem Maximal.eq_of_ge {α : Type u_1} {P : αProp} {x : α} {y : α} [PartialOrder α] (hx : Maximal P x) (hy : P y) (hge : x y) :
      y = x
      theorem minimal_iff {α : Type u_1} {P : αProp} {x : α} [PartialOrder α] :
      Minimal P x P x ∀ ⦃y : α⦄, P yy xx = y
      theorem maximal_iff {α : Type u_1} {P : αProp} {x : α} [PartialOrder α] :
      Maximal P x P x ∀ ⦃y : α⦄, P yx yx = y
      theorem minimal_mem_iff {α : Type u_1} {x : α} [PartialOrder α] {s : Set α} :
      Minimal (fun (x : α) => x s) x x s ∀ ⦃y : α⦄, y sy xx = y
      theorem maximal_mem_iff {α : Type u_1} {x : α} [PartialOrder α] {s : Set α} :
      Maximal (fun (x : α) => x s) x x s ∀ ⦃y : α⦄, y sx yx = y
      theorem minimal_iff_eq {α : Type u_1} {P : αProp} {x : α} {y : α} [PartialOrder α] (hy : P y) (hP : ∀ ⦃x : α⦄, P xy x) :
      Minimal P x x = y

      If P y holds, and everything satisfying P is above y, then y is the unique minimal element satisfying P.

      theorem maximal_iff_eq {α : Type u_1} {P : αProp} {x : α} {y : α} [PartialOrder α] (hy : P y) (hP : ∀ ⦃x : α⦄, P xx y) :
      Maximal P x x = y

      If P y holds, and everything satisfying P is below y, then y is the unique maximal element satisfying P.

      @[simp]
      theorem minimal_ge_iff {α : Type u_1} {x : α} {y : α} [PartialOrder α] :
      Minimal (fun (x : α) => y x) x x = y
      @[simp]
      theorem maximal_le_iff {α : Type u_1} {x : α} {y : α} [PartialOrder α] :
      Maximal (fun (x : α) => x y) x x = y
      theorem minimal_iff_minimal_of_imp_of_forall {α : Type u_1} {P : αProp} {Q : αProp} {x : α} [PartialOrder α] (hPQ : ∀ ⦃x : α⦄, Q xP x) (h : ∀ ⦃x : α⦄, P xyx, Q y) :
      theorem maximal_iff_maximal_of_imp_of_forall {α : Type u_1} {P : αProp} {Q : αProp} {x : α} [PartialOrder α] (hPQ : ∀ ⦃x : α⦄, Q xP x) (h : ∀ ⦃x : α⦄, P x∃ (y : α), x y Q y) :
      theorem Minimal.eq_of_superset {α : Type u_1} {P : Set αProp} {s : Set α} {t : Set α} (h : Minimal P s) (ht : P t) (hts : t s) :
      s = t
      theorem Maximal.eq_of_subset {α : Type u_1} {P : Set αProp} {s : Set α} {t : Set α} (h : Maximal P s) (ht : P t) (hst : s t) :
      s = t
      theorem Minimal.eq_of_subset {α : Type u_1} {P : Set αProp} {s : Set α} {t : Set α} (h : Minimal P s) (ht : P t) (hts : t s) :
      t = s
      theorem Maximal.eq_of_superset {α : Type u_1} {P : Set αProp} {s : Set α} {t : Set α} (h : Maximal P s) (ht : P t) (hst : s t) :
      t = s
      theorem minimal_subset_iff {α : Type u_1} {P : Set αProp} {s : Set α} :
      Minimal P s P s ∀ ⦃t : Set α⦄, P tt ss = t
      theorem maximal_subset_iff {α : Type u_1} {P : Set αProp} {s : Set α} :
      Maximal P s P s ∀ ⦃t : Set α⦄, P ts ts = t
      theorem minimal_subset_iff' {α : Type u_1} {P : Set αProp} {s : Set α} :
      Minimal P s P s ∀ ⦃t : Set α⦄, P tt ss t
      theorem maximal_subset_iff' {α : Type u_1} {P : Set αProp} {s : Set α} :
      Maximal P s P s ∀ ⦃t : Set α⦄, P ts tt s
      theorem not_minimal_subset_iff {α : Type u_1} {P : Set αProp} {s : Set α} (hs : P s) :
      ¬Minimal P s ts, P t
      theorem not_maximal_subset_iff {α : Type u_1} {P : Set αProp} {s : Set α} (hs : P s) :
      ¬Maximal P s ∃ (t : Set α), s t P t
      theorem Set.minimal_iff_forall_ssubset {α : Type u_1} {P : Set αProp} {s : Set α} :
      Minimal P s P s ∀ ⦃t : Set α⦄, t s¬P t
      theorem Minimal.not_prop_of_ssubset {α : Type u_1} {P : Set αProp} {s : Set α} {t : Set α} (h : Minimal P s) (ht : t s) :
      ¬P t
      theorem Minimal.not_ssubset {α : Type u_1} {P : Set αProp} {s : Set α} {t : Set α} (h : Minimal P s) (ht : P t) :
      ¬t s
      theorem Maximal.mem_of_prop_insert {α : Type u_1} {x : α} {P : Set αProp} {s : Set α} (h : Maximal P s) (hx : P (insert x s)) :
      x s
      theorem Minimal.not_mem_of_prop_diff_singleton {α : Type u_1} {x : α} {P : Set αProp} {s : Set α} (h : Minimal P s) (hx : P (s \ {x})) :
      xs
      theorem Set.minimal_iff_forall_diff_singleton {α : Type u_1} {P : Set αProp} {s : Set α} (hP : ∀ ⦃s t : Set α⦄, P tt sP s) :
      Minimal P s P s xs, ¬P (s \ {x})
      theorem Set.exists_diff_singleton_of_not_minimal {α : Type u_1} {P : Set αProp} {s : Set α} (hP : ∀ ⦃s t : Set α⦄, P tt sP s) (hs : P s) (h : ¬Minimal P s) :
      xs, P (s \ {x})
      theorem Set.maximal_iff_forall_ssuperset {α : Type u_1} {P : Set αProp} {s : Set α} :
      Maximal P s P s ∀ ⦃t : Set α⦄, s t¬P t
      theorem Maximal.not_prop_of_ssuperset {α : Type u_1} {P : Set αProp} {s : Set α} {t : Set α} (h : Maximal P s) (ht : s t) :
      ¬P t
      theorem Maximal.not_ssuperset {α : Type u_1} {P : Set αProp} {s : Set α} {t : Set α} (h : Maximal P s) (ht : P t) :
      ¬s t
      theorem Set.maximal_iff_forall_insert {α : Type u_1} {P : Set αProp} {s : Set α} (hP : ∀ ⦃s t : Set α⦄, P ts tP s) :
      Maximal P s P s xs, ¬P (insert x s)
      theorem Set.exists_insert_of_not_maximal {α : Type u_1} {P : Set αProp} {s : Set α} (hP : ∀ ⦃s t : Set α⦄, P ts tP s) (hs : P s) (h : ¬Maximal P s) :
      xs, P (insert x s)
      theorem setOf_minimal_subset {α : Type u_1} [Preorder α] (s : Set α) :
      {x : α | Minimal (fun (x : α) => x s) x} s
      theorem setOf_maximal_subset {α : Type u_1} [Preorder α] (s : Set α) :
      {x : α | Maximal (fun (x : α) => x s) x} s
      theorem Set.Subsingleton.maximal_mem_iff {α : Type u_1} {x : α} {s : Set α} [Preorder α] (h : s.Subsingleton) :
      Maximal (fun (x : α) => x s) x x s
      theorem Set.Subsingleton.minimal_mem_iff {α : Type u_1} {x : α} {s : Set α} [Preorder α] (h : s.Subsingleton) :
      Minimal (fun (x : α) => x s) x x s
      theorem IsLeast.minimal {α : Type u_1} {x : α} {s : Set α} [Preorder α] (h : IsLeast s x) :
      Minimal (fun (x : α) => x s) x
      theorem IsGreatest.maximal {α : Type u_1} {x : α} {s : Set α} [Preorder α] (h : IsGreatest s x) :
      Maximal (fun (x : α) => x s) x
      theorem IsAntichain.minimal_mem_iff {α : Type u_1} {x : α} {s : Set α} [Preorder α] (hs : IsAntichain (fun (x1 x2 : α) => x1 x2) s) :
      Minimal (fun (x : α) => x s) x x s
      theorem IsAntichain.maximal_mem_iff {α : Type u_1} {x : α} {s : Set α} [Preorder α] (hs : IsAntichain (fun (x1 x2 : α) => x1 x2) s) :
      Maximal (fun (x : α) => x s) x x s
      theorem IsAntichain.eq_setOf_maximal {α : Type u_1} {s : Set α} {t : Set α} [Preorder α] (ht : IsAntichain (fun (x1 x2 : α) => x1 x2) t) (h : ∀ (x : α), Maximal (fun (x : α) => x s) xx t) (hs : at, ba, Maximal (fun (x : α) => x s) b) :
      {x : α | Maximal (fun (x : α) => x s) x} = t

      If t is an antichain shadowing and including the set of maximal elements of s, then t is the set of maximal elements of s.

      theorem IsAntichain.eq_setOf_minimal {α : Type u_1} {s : Set α} {t : Set α} [Preorder α] (ht : IsAntichain (fun (x1 x2 : α) => x1 x2) t) (h : ∀ (x : α), Minimal (fun (x : α) => x s) xx t) (hs : at, ∃ (b : α), a b Minimal (fun (x : α) => x s) b) :
      {x : α | Minimal (fun (x : α) => x s) x} = t

      If t is an antichain shadowed by and including the set of minimal elements of s, then t is the set of minimal elements of s.

      theorem setOf_maximal_antichain {α : Type u_1} [PartialOrder α] (P : αProp) :
      IsAntichain (fun (x1 x2 : α) => x1 x2) {x : α | Maximal P x}
      theorem setOf_minimal_antichain {α : Type u_1} [PartialOrder α] (P : αProp) :
      IsAntichain (fun (x1 x2 : α) => x1 x2) {x : α | Minimal P x}
      theorem IsAntichain.minimal_mem_upperClosure_iff_mem {α : Type u_1} {x : α} {s : Set α} [PartialOrder α] (hs : IsAntichain (fun (x1 x2 : α) => x1 x2) s) :
      Minimal (fun (x : α) => x upperClosure s) x x s
      theorem IsAntichain.maximal_mem_lowerClosure_iff_mem {α : Type u_1} {x : α} {s : Set α} [PartialOrder α] (hs : IsAntichain (fun (x1 x2 : α) => x1 x2) s) :
      Maximal (fun (x : α) => x lowerClosure s) x x s
      theorem IsLeast.minimal_iff {α : Type u_1} {a : α} {x : α} {s : Set α} [PartialOrder α] (h : IsLeast s a) :
      Minimal (fun (x : α) => x s) x x = a
      theorem IsGreatest.maximal_iff {α : Type u_1} {a : α} {x : α} {s : Set α} [PartialOrder α] (h : IsGreatest s a) :
      Maximal (fun (x : α) => x s) x x = a
      theorem minimal_mem_image_monotone {α : Type u_1} {x : α} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {f : αβ} (hf : ∀ ⦃x y : α⦄, x sy s(f x f y x y)) (hx : Minimal (fun (x : α) => x s) x) :
      Minimal (fun (x : β) => x f '' s) (f x)
      theorem maximal_mem_image_monotone {α : Type u_1} {x : α} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {f : αβ} (hf : ∀ ⦃x y : α⦄, x sy s(f x f y x y)) (hx : Maximal (fun (x : α) => x s) x) :
      Maximal (fun (x : β) => x f '' s) (f x)
      theorem minimal_mem_image_monotone_iff {α : Type u_1} {a : α} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {f : αβ} (ha : a s) (hf : ∀ ⦃x y : α⦄, x sy s(f x f y x y)) :
      Minimal (fun (x : β) => x f '' s) (f a) Minimal (fun (x : α) => x s) a
      theorem maximal_mem_image_monotone_iff {α : Type u_1} {a : α} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {f : αβ} (ha : a s) (hf : ∀ ⦃x y : α⦄, x sy s(f x f y x y)) :
      Maximal (fun (x : β) => x f '' s) (f a) Maximal (fun (x : α) => x s) a
      theorem minimal_mem_image_antitone {α : Type u_1} {x : α} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {f : αβ} (hf : ∀ ⦃x y : α⦄, x sy s(f x f y y x)) (hx : Minimal (fun (x : α) => x s) x) :
      Maximal (fun (x : β) => x f '' s) (f x)
      theorem maximal_mem_image_antitone {α : Type u_1} {x : α} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {f : αβ} (hf : ∀ ⦃x y : α⦄, x sy s(f x f y y x)) (hx : Maximal (fun (x : α) => x s) x) :
      Minimal (fun (x : β) => x f '' s) (f x)
      theorem minimal_mem_image_antitone_iff {α : Type u_1} {a : α} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {f : αβ} (ha : a s) (hf : ∀ ⦃x y : α⦄, x sy s(f x f y y x)) :
      Minimal (fun (x : β) => x f '' s) (f a) Maximal (fun (x : α) => x s) a
      theorem maximal_mem_image_antitone_iff {α : Type u_1} {a : α} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {f : αβ} (ha : a s) (hf : ∀ ⦃x y : α⦄, x sy s(f x f y y x)) :
      Maximal (fun (x : β) => x f '' s) (f a) Minimal (fun (x : α) => x s) a
      theorem image_monotone_setOf_minimal {α : Type u_1} {P : αProp} [Preorder α] {β : Type u_2} [Preorder β] {f : αβ} (hf : ∀ ⦃x y : α⦄, P xP y(f x f y x y)) :
      f '' {x : α | Minimal P x} = {x : β | Minimal (fun (x : β) => ∃ (x₀ : α), P x₀ f x₀ = x) x}
      theorem image_monotone_setOf_maximal {α : Type u_1} {P : αProp} [Preorder α] {β : Type u_2} [Preorder β] {f : αβ} (hf : ∀ ⦃x y : α⦄, P xP y(f x f y x y)) :
      f '' {x : α | Maximal P x} = {x : β | Maximal (fun (x : β) => ∃ (x₀ : α), P x₀ f x₀ = x) x}
      theorem image_antitone_setOf_minimal {α : Type u_1} {P : αProp} [Preorder α] {β : Type u_2} [Preorder β] {f : αβ} (hf : ∀ ⦃x y : α⦄, P xP y(f x f y y x)) :
      f '' {x : α | Minimal P x} = {x : β | Maximal (fun (x : β) => ∃ (x₀ : α), P x₀ f x₀ = x) x}
      theorem image_antitone_setOf_maximal {α : Type u_1} {P : αProp} [Preorder α] {β : Type u_2} [Preorder β] {f : αβ} (hf : ∀ ⦃x y : α⦄, P xP y(f x f y y x)) :
      f '' {x : α | Maximal P x} = {x : β | Minimal (fun (x : β) => ∃ (x₀ : α), P x₀ f x₀ = x) x}
      theorem image_monotone_setOf_minimal_mem {α : Type u_1} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {f : αβ} (hf : ∀ ⦃x y : α⦄, x sy s(f x f y x y)) :
      f '' {x : α | Minimal (fun (x : α) => x s) x} = {x : β | Minimal (fun (x : β) => x f '' s) x}
      theorem image_monotone_setOf_maximal_mem {α : Type u_1} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {f : αβ} (hf : ∀ ⦃x y : α⦄, x sy s(f x f y x y)) :
      f '' {x : α | Maximal (fun (x : α) => x s) x} = {x : β | Maximal (fun (x : β) => x f '' s) x}
      theorem image_antitone_setOf_minimal_mem {α : Type u_1} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {f : αβ} (hf : ∀ ⦃x y : α⦄, x sy s(f x f y y x)) :
      f '' {x : α | Minimal (fun (x : α) => x s) x} = {x : β | Maximal (fun (x : β) => x f '' s) x}
      theorem image_antitone_setOf_maximal_mem {α : Type u_1} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {f : αβ} (hf : ∀ ⦃x y : α⦄, x sy s(f x f y y x)) :
      f '' {x : α | Maximal (fun (x : α) => x s) x} = {x : β | Minimal (fun (x : β) => x f '' s) x}
      theorem OrderEmbedding.minimal_mem_image {α : Type u_1} {x : α} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} (f : α ↪o β) (hx : Minimal (fun (x : α) => x s) x) :
      Minimal (fun (x : β) => x f '' s) (f x)
      theorem OrderEmbedding.maximal_mem_image {α : Type u_1} {x : α} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} (f : α ↪o β) (hx : Maximal (fun (x : α) => x s) x) :
      Maximal (fun (x : β) => x f '' s) (f x)
      theorem OrderEmbedding.minimal_mem_image_iff {α : Type u_1} {a : α} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {f : α ↪o β} (ha : a s) :
      Minimal (fun (x : β) => x f '' s) (f a) Minimal (fun (x : α) => x s) a
      theorem OrderEmbedding.maximal_mem_image_iff {α : Type u_1} {a : α} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {f : α ↪o β} (ha : a s) :
      Maximal (fun (x : β) => x f '' s) (f a) Maximal (fun (x : α) => x s) a
      theorem OrderEmbedding.minimal_apply_mem_inter_range_iff {α : Type u_1} {x : α} [Preorder α] {β : Type u_2} [Preorder β] {f : α ↪o β} {t : Set β} :
      Minimal (fun (x : β) => x t Set.range f) (f x) Minimal (fun (x : α) => f x t) x
      theorem OrderEmbedding.maximal_apply_mem_inter_range_iff {α : Type u_1} {x : α} [Preorder α] {β : Type u_2} [Preorder β] {f : α ↪o β} {t : Set β} :
      Maximal (fun (x : β) => x t Set.range f) (f x) Maximal (fun (x : α) => f x t) x
      theorem OrderEmbedding.minimal_apply_mem_iff {α : Type u_1} {x : α} [Preorder α] {β : Type u_2} [Preorder β] {f : α ↪o β} {t : Set β} (ht : t Set.range f) :
      Minimal (fun (x : β) => x t) (f x) Minimal (fun (x : α) => f x t) x
      theorem OrderEmbedding.maximal_apply_iff {α : Type u_1} {x : α} [Preorder α] {β : Type u_2} [Preorder β] {f : α ↪o β} {t : Set β} (ht : t Set.range f) :
      Maximal (fun (x : β) => x t) (f x) Maximal (fun (x : α) => f x t) x
      @[simp]
      theorem OrderEmbedding.image_setOf_minimal {α : Type u_1} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {f : α ↪o β} :
      f '' {x : α | Minimal (fun (x : α) => x s) x} = {x : β | Minimal (fun (x : β) => x f '' s) x}
      @[simp]
      theorem OrderEmbedding.image_setOf_maximal {α : Type u_1} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {f : α ↪o β} :
      f '' {x : α | Maximal (fun (x : α) => x s) x} = {x : β | Maximal (fun (x : β) => x f '' s) x}
      theorem OrderEmbedding.inter_preimage_setOf_minimal_eq_of_subset {α : Type u_1} {x : α} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {f : α ↪o β} {t : Set β} (hts : t f '' s) :
      x s f ⁻¹' {y : β | Minimal (fun (x : β) => x t) y} Minimal (fun (x : α) => x s f ⁻¹' t) x
      theorem OrderEmbedding.inter_preimage_setOf_maximal_eq_of_subset {α : Type u_1} {x : α} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {f : α ↪o β} {t : Set β} (hts : t f '' s) :
      x s f ⁻¹' {y : β | Maximal (fun (x : β) => x t) y} Maximal (fun (x : α) => x s f ⁻¹' t) x
      theorem OrderIso.image_setOf_minimal {α : Type u_1} [Preorder α] {β : Type u_2} [Preorder β] (f : α ≃o β) (P : αProp) :
      f '' {x : α | Minimal P x} = {x : β | Minimal (fun (x : β) => P (f.symm x)) x}
      theorem OrderIso.image_setOf_maximal {α : Type u_1} [Preorder α] {β : Type u_2} [Preorder β] (f : α ≃o β) (P : αProp) :
      f '' {x : α | Maximal P x} = {x : β | Maximal (fun (x : β) => P (f.symm x)) x}
      theorem OrderIso.map_minimal_mem {α : Type u_1} {x : α} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {t : Set β} (f : s ≃o t) (hx : Minimal (fun (x : α) => x s) x) :
      Minimal (fun (x : β) => x t) (f x, )
      theorem OrderIso.map_maximal_mem {α : Type u_1} {x : α} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {t : Set β} (f : s ≃o t) (hx : Maximal (fun (x : α) => x s) x) :
      Maximal (fun (x : β) => x t) (f x, )
      def OrderIso.mapSetOfMinimal {α : Type u_1} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {t : Set β} (f : s ≃o t) :
      {x : α | Minimal (fun (x : α) => x s) x} ≃o {x : β | Minimal (fun (x : β) => x t) x}

      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.mapSetOfMaximal {α : Type u_1} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {t : Set β} (f : s ≃o t) :
        {x : α | Maximal (fun (x : α) => x s) x} ≃o {x : β | Maximal (fun (x : β) => x t) x}

        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.setOfMinimalIsoSetOfMaximal {α : Type u_1} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {t : Set β} (f : s ≃o (↑t)ᵒᵈ) :
          {x : α | Minimal (fun (x : α) => x s) x} ≃o {x : βᵒᵈ | Maximal (fun (x : β) => x t) (OrderDual.ofDual x)}

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def OrderIso.setOfMaximalIsoSetOfMinimal {α : Type u_1} [Preorder α] {β : Type u_2} [Preorder β] {s : Set α} {t : Set β} (f : s ≃o (↑t)ᵒᵈ) :
            {x : α | Maximal (fun (x : α) => x s) x} ≃o {x : βᵒᵈ | Minimal (fun (x : β) => x t) (OrderDual.ofDual x)}

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

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem minimal_mem_Icc {α : Type u_1} {x : α} [PartialOrder α] {a : α} {b : α} (hab : a b) :
              Minimal (fun (x : α) => x Set.Icc a b) x x = a
              theorem maximal_mem_Icc {α : Type u_1} {x : α} [PartialOrder α] {a : α} {b : α} (hab : a b) :
              Maximal (fun (x : α) => x Set.Icc a b) x x = b
              theorem minimal_mem_Ico {α : Type u_1} {x : α} [PartialOrder α] {a : α} {b : α} (hab : a < b) :
              Minimal (fun (x : α) => x Set.Ico a b) x x = a
              theorem maximal_mem_Ioc {α : Type u_1} {x : α} [PartialOrder α] {a : α} {b : α} (hab : a < b) :
              Maximal (fun (x : α) => x Set.Ioc a b) x x = b