Minimality and Maximality

This file proves basic facts about minimality and maximality of an element with respect to a predicate P on an ordered type α.

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

• In the linearly ordered case, versions of lemmas like minimal_mem_image will hold with MonotoneOn/AntitoneOn assumptions rather than the stronger x ≤ y ↔ f x ≤ f y assumptions.

• Set.maximal_iff_forall_insert and Set.minimal_iff_forall_diff_singleton will generalize to lemmas about covering in the case of an IsStronglyAtomic/IsStronglyCoatomic order.

• Finset versions of the lemmas about sets.

• API to allow for easily expressing min/maximality with respect to an arbitrary non-LE relation.

@[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 x → Minimal (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 x → Maximal (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 α] : Minimal (Minimal P) x ↔ Minimal P x

@[simp]

theorem maximal_maximal {α : Type u_1} {P : α → Prop} {x : α} [LE α] : Maximal (Maximal P) x ↔ Maximal P x

theorem minimal_iff_isMin {α : Type u_1} {P : α → Prop} {x : α} [LE α] (hP : ∀ ⦃x y : α⦄, P y → x ≤ y → P 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 y → y ≤ x → P 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) : Minimal Q x

theorem Maximal.mono {α : Type u_1} {P : α → Prop} {Q : α → Prop} {x : α} [LE α] (h : Maximal P x) (hle : Q ≤ P) (hQ : Q x) : Maximal 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) : Minimal P x ∨ Minimal Q x

theorem Maximal.or {α : Type u_1} {P : α → Prop} {Q : α → Prop} {x : α} [LE α] (h : Maximal (fun (x : α) => P x ∨ Q x) x) : Maximal P x ∨ Maximal Q x

theorem minimal_and_iff_right_of_imp {α : Type u_1} {P : α → Prop} {Q : α → Prop} {x : α} [LE α] (hPQ : ∀ ⦃x : α⦄, P x → Q 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 x → Q 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 x → Q 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 x → Q 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 x → ∃ y < 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 y → y ≤ x → x = y

theorem maximal_iff {α : Type u_1} {P : α → Prop} {x : α} [PartialOrder α] : Maximal P x ↔ P x ∧ ∀ ⦃y : α⦄, P y → x ≤ y → x = y

theorem minimal_mem_iff {α : Type u_1} {x : α} [PartialOrder α] {s : Set α} : Minimal (fun (x : α) => x ∈ s) x ↔ x ∈ s ∧ ∀ ⦃y : α⦄, y ∈ s → y ≤ x → x = y

theorem maximal_mem_iff {α : Type u_1} {x : α} [PartialOrder α] {s : Set α} : Maximal (fun (x : α) => x ∈ s) x ↔ x ∈ s ∧ ∀ ⦃y : α⦄, y ∈ s → x ≤ y → x = y

theorem minimal_iff_eq {α : Type u_1} {P : α → Prop} {x : α} {y : α} [PartialOrder α] (hy : P y) (hP : ∀ ⦃x : α⦄, P x → y ≤ 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 x → x ≤ 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 x → P x) (h : ∀ ⦃x : α⦄, P x → ∃ y ≤ x, Q y) : Minimal P x ↔ Minimal Q x

theorem maximal_iff_maximal_of_imp_of_forall {α : Type u_1} {P : α → Prop} {Q : α → Prop} {x : α} [PartialOrder α] (hPQ : ∀ ⦃x : α⦄, Q x → P x) (h : ∀ ⦃x : α⦄, P x → ∃ (y : α), x ≤ y ∧ Q y) : Maximal P x ↔ Maximal Q x

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 t → t ⊆ s → s = t

theorem maximal_subset_iff {α : Type u_1} {P : Set α → Prop} {s : Set α} : Maximal P s ↔ P s ∧ ∀ ⦃t : Set α⦄, P t → s ⊆ t → s = t

theorem minimal_subset_iff' {α : Type u_1} {P : Set α → Prop} {s : Set α} : Minimal P s ↔ P s ∧ ∀ ⦃t : Set α⦄, P t → t ⊆ s → s ⊆ t

theorem maximal_subset_iff' {α : Type u_1} {P : Set α → Prop} {s : Set α} : Maximal P s ↔ P s ∧ ∀ ⦃t : Set α⦄, P t → s ⊆ t → t ⊆ s

theorem not_minimal_subset_iff {α : Type u_1} {P : Set α → Prop} {s : Set α} (hs : P s) : ¬Minimal P s ↔ ∃ t ⊂ s, 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})) : x ∉ s

theorem Set.minimal_iff_forall_diff_singleton {α : Type u_1} {P : Set α → Prop} {s : Set α} (hP : ∀ ⦃s t : Set α⦄, P t → t ⊆ s → P s) : Minimal P s ↔ P s ∧ ∀ x ∈ s, ¬P (s \ {x})

theorem Set.exists_diff_singleton_of_not_minimal {α : Type u_1} {P : Set α → Prop} {s : Set α} (hP : ∀ ⦃s t : Set α⦄, P t → t ⊆ s → P s) (hs : P s) (h : ¬Minimal P s) : ∃ x ∈ s, 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 t → s ⊆ t → P s) : Maximal P s ↔ P s ∧ ∀ x ∉ s, ¬P (insert x s)

theorem Set.exists_insert_of_not_maximal {α : Type u_1} {P : Set α → Prop} {s : Set α} (hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s) (hs : P s) (h : ¬Maximal P s) : ∃ x ∉ s, 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) x → x ∈ t) (hs : ∀ a ∈ t, ∃ b ≤ a, 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) x → x ∈ t) (hs : ∀ a ∈ t, ∃ (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 ∈ s → y ∈ 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 ∈ s → y ∈ 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 ∈ s → y ∈ 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 ∈ s → y ∈ 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 ∈ s → y ∈ 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 ∈ s → y ∈ 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 ∈ s → y ∈ 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 ∈ s → y ∈ 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 x → P 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 x → P 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 x → P 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 x → P 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 ∈ s → y ∈ 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 ∈ s → y ∈ 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 ∈ s → y ∈ 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 ∈ s → y ∈ 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.

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.

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.

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.

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