# 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.

- API for `MinimalFor`/`MaximalFor`

source
@[simp]
theorem minimalFor_eq_iff {ι : Type u_1} {α : Type u_2} [LE α] {f : ι → α} {i j : ι} :
MinimalFor (fun (x : ι) => x = j) f i ↔ i = j
source
@[simp]
theorem maximalFor_eq_iff {ι : Type u_1} {α : Type u_2} [LE α] {f : ι → α} {i j : ι} :
MaximalFor (fun (x : ι) => x = j) f i ↔ i = j
source
@[simp]
theorem minimalFor_id {α : Type u_2} {P : α → Prop} {x : α} [LE α] :
MinimalFor P id x ↔ Minimal P x
source
@[simp]
theorem maximalFor_id {α : Type u_2} {P : α → Prop} {x : α} [LE α] :
MaximalFor P id x ↔ Maximal P x
source
@[simp]
theorem minimal_toDual {α : Type u_2} {P : α → Prop} {x : α} [LE α] :
Minimal (fun (x : α ᵒᵈ) => P (OrderDual.ofDual x)) (OrderDual.toDual x) ↔ Maximal P x
source
theorem Minimal.of_dual {α : Type u_2} {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`.

source
theorem Minimal.dual {α : Type u_2} {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`.

source
@[simp]
theorem maximal_toDual {α : Type u_2} {P : α → Prop} {x : α} [LE α] :
Maximal (fun (x : α ᵒᵈ) => P (OrderDual.ofDual x)) (OrderDual.toDual x) ↔ Minimal P x
source
theorem Maximal.dual {α : Type u_2} {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`.

source
theorem Maximal.of_dual {α : Type u_2} {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`.

source
@[simp]
theorem minimal_false {α : Type u_2} {x : α} [LE α] :
¬Minimal (fun (x : α) => False) x
source
@[simp]
theorem maximal_false {α : Type u_2} {x : α} [LE α] :
¬Maximal (fun (x : α) => False) x
source
@[simp]
theorem minimal_true {α : Type u_2} {x : α} [LE α] :
Minimal (fun (x : α) => True) x ↔ IsMin x
source
@[simp]
theorem maximal_true {α : Type u_2} {x : α} [LE α] :
Maximal (fun (x : α) => True) x ↔ IsMax x
source
@[simp]
theorem minimal_subtype {α : Type u_2} {P Q : α → Prop} [LE α] {x : Subtype Q} :
Minimal (fun (x : Subtype Q) => P ↑x) x ↔ Minimal (P ⊓ Q) ↑x
source
@[simp]
theorem maximal_subtype {α : Type u_2} {P Q : α → Prop} [LE α] {x : Subtype Q} :
Maximal (fun (x : Subtype Q) => P ↑x) x ↔ Maximal (P ⊓ Q) ↑x
source
theorem maximal_true_subtype {α : Type u_2} {P : α → Prop} [LE α] {x : Subtype P} :
Maximal (fun (x : Subtype P) => True) x ↔ Maximal P ↑x
source
theorem minimal_true_subtype {α : Type u_2} {P : α → Prop} [LE α] {x : Subtype P} :
Minimal (fun (x : Subtype P) => True) x ↔ Minimal P ↑x
source
@[simp]
theorem minimal_minimal {α : Type u_2} {P : α → Prop} {x : α} [LE α] :
Minimal (Minimal P) x ↔ Minimal P x
source
@[simp]
theorem maximal_maximal {α : Type u_2} {P : α → Prop} {x : α} [LE α] :
Maximal (Maximal P) x ↔ Maximal P x
source
theorem minimal_iff_isMin {α : Type u_2} {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`.

source
theorem maximal_iff_isMax {α : Type u_2} {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`.

source
theorem Minimal.mono {α : Type u_2} {P Q : α → Prop} {x : α} [LE α] (h : Minimal P x) (hle : Q ≤ P) (hQ : Q x) :
Minimal Q x
source
theorem Maximal.mono {α : Type u_2} {P Q : α → Prop} {x : α} [LE α] (h : Maximal P x) (hle : Q ≤ P) (hQ : Q x) :
Maximal Q x
source
theorem Minimal.and_right {α : Type u_2} {P Q : α → Prop} {x : α} [LE α] (h : Minimal P x) (hQ : Q x) :
Minimal (fun (x : α) => P x ∧ Q x) x
source
theorem Minimal.and_left {α : Type u_2} {P Q : α → Prop} {x : α} [LE α] (h : Minimal P x) (hQ : Q x) :
Minimal (fun (x : α) => Q x ∧ P x) x
source
theorem Maximal.and_right {α : Type u_2} {P Q : α → Prop} {x : α} [LE α] (h : Maximal P x) (hQ : Q x) :
Maximal (fun (x : α) => P x ∧ Q x) x
source
theorem Maximal.and_left {α : Type u_2} {P Q : α → Prop} {x : α} [LE α] (h : Maximal P x) (hQ : Q x) :
Maximal (fun (x : α) => Q x ∧ P x) x
source
@[simp]
theorem minimal_eq_iff {α : Type u_2} {x y : α} [LE α] :
Minimal (fun (x : α) => x = y) x ↔ x = y
source
@[simp]
theorem maximal_eq_iff {α : Type u_2} {x y : α} [LE α] :
Maximal (fun (x : α) => x = y) x ↔ x = y
source
theorem not_minimal_iff {α : Type u_2} {P : α → Prop} {x : α} [LE α] (hx : P x) :
¬Minimal P x ↔ ∃ (y : α), P y ∧ y ≤ x ∧ ¬x ≤ y
source
theorem not_maximal_iff {α : Type u_2} {P : α → Prop} {x : α} [LE α] (hx : P x) :
¬Maximal P x ↔ ∃ (y : α), P y ∧ x ≤ y ∧ ¬y ≤ x
source
theorem Minimal.or {α : Type u_2} {P Q : α → Prop} {x : α} [LE α] (h : Minimal (fun (x : α) => P x ∨ Q x) x) :
Minimal P x ∨ Minimal Q x
source
theorem Maximal.or {α : Type u_2} {P Q : α → Prop} {x : α} [LE α] (h : Maximal (fun (x : α) => P x ∨ Q x) x) :
Maximal P x ∨ Maximal Q x
source
theorem minimal_and_iff_right_of_imp {α : Type u_2} {P Q : α → Prop} {x : α} [LE α] (hPQ : ∀ ⦃x : α⦄, P x → Q x) :
Minimal (fun (x : α) => P x ∧ Q x) x ↔ Minimal P x ∧ Q x
source
theorem minimal_and_iff_left_of_imp {α : Type u_2} {P Q : α → Prop} {x : α} [LE α] (hPQ : ∀ ⦃x : α⦄, P x → Q x) :
Minimal (fun (x : α) => Q x ∧ P x) x ↔ Q x ∧ Minimal P x
source
theorem maximal_and_iff_right_of_imp {α : Type u_2} {P Q : α → Prop} {x : α} [LE α] (hPQ : ∀ ⦃x : α⦄, P x → Q x) :
Maximal (fun (x : α) => P x ∧ Q x) x ↔ Maximal P x ∧ Q x
source
theorem maximal_and_iff_left_of_imp {α : Type u_2} {P Q : α → Prop} {x : α} [LE α] (hPQ : ∀ ⦃x : α⦄, P x → Q x) :
Maximal (fun (x : α) => Q x ∧ P x) x ↔ Q x ∧ Maximal P x
source
theorem minimal_iff_forall_lt {α : Type u_2} {P : α → Prop} {x : α} [Preorder α] :
Minimal P x ↔ P x ∧ ∀ ⦃y : α⦄, y < x → ¬P y
source
theorem maximal_iff_forall_gt {α : Type u_2} {P : α → Prop} {x : α} [Preorder α] :
Maximal P x ↔ P x ∧ ∀ ⦃y : α⦄, x < y → ¬P y
source
theorem Minimal.not_prop_of_lt {α : Type u_2} {P : α → Prop} {x y : α} [Preorder α] (h : Minimal P x) (hlt : y < x) :
¬P y
source
theorem Maximal.not_prop_of_gt {α : Type u_2} {P : α → Prop} {x y : α} [Preorder α] (h : Maximal P x) (hlt : x < y) :
¬P y
source
theorem Minimal.not_lt {α : Type u_2} {P : α → Prop} {x y : α} [Preorder α] (h : Minimal P x) (hy : P y) :
¬y < x
source
theorem Maximal.not_gt {α : Type u_2} {P : α → Prop} {x y : α} [Preorder α] (h : Maximal P x) (hy : P y) :
¬x < y
source
@[simp]
theorem minimal_le_iff {α : Type u_2} {x y : α} [Preorder α] :
Minimal (fun (x : α) => x ≤ y) x ↔ x ≤ y ∧ IsMin x
source
@[simp]
theorem maximal_ge_iff {α : Type u_2} {x y : α} [Preorder α] :
Maximal (fun (x : α) => y ≤ x) x ↔ y ≤ x ∧ IsMax x
source
@[simp]
theorem minimal_lt_iff {α : Type u_2} {x y : α} [Preorder α] :
Minimal (fun (x : α) => x < y) x ↔ x < y ∧ IsMin x
source
@[simp]
theorem maximal_gt_iff {α : Type u_2} {x y : α} [Preorder α] :
Maximal (fun (x : α) => y < x) x ↔ y < x ∧ IsMax x
source
theorem not_minimal_iff_exists_lt {α : Type u_2} {P : α → Prop} {x : α} [Preorder α] (hx : P x) :
¬Minimal P x ↔ ∃ y < x, P y
source
theorem exists_lt_of_not_minimal {α : Type u_2} {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`.

source
theorem not_maximal_iff_exists_gt {α : Type u_2} {P : α → Prop} {x : α} [Preorder α] (hx : P x) :
¬Maximal P x ↔ ∃ (y : α), x < y ∧ P y
source
theorem exists_gt_of_not_maximal {α : Type u_2} {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`.

source
theorem exists_minimalFor_of_wellFoundedLT {ι : Type u_1} {α : Type u_2} [Preorder α] [WellFoundedLT α] (P : ι → Prop) (f : ι → α) (hP : ∃ (i : ι), P i) :
∃ (i : ι), MinimalFor P f i
source
theorem exists_minimal_of_wellFoundedLT {α : Type u_2} [Preorder α] [WellFoundedLT α] (P : α → Prop) (hP : ∃ (a : α), P a) :
∃ (a : α), Minimal P a
source
theorem exists_minimal_le_of_wellFoundedLT {α : Type u_2} [Preorder α] [WellFoundedLT α] (P : α → Prop) (a : α) (ha : P a) :
∃ b ≤ a, Minimal P b
source
theorem exists_maximalFor_of_wellFoundedGT {ι : Type u_1} {α : Type u_2} [Preorder α] [WellFoundedGT α] (P : ι → Prop) (f : ι → α) (hP : ∃ (i : ι), P i) :
∃ (i : ι), MaximalFor P f i
source
theorem exists_maximal_of_wellFoundedGT {α : Type u_2} [Preorder α] [WellFoundedGT α] (P : α → Prop) (hP : ∃ (a : α), P a) :
∃ (a : α), Maximal P a
source
theorem exists_maximal_ge_of_wellFoundedGT {α : Type u_2} [Preorder α] [WellFoundedGT α] (P : α → Prop) (a : α) (ha : P a) :
∃ (b : α), a ≤ b ∧ Maximal P b
source
theorem Minimal.eq_of_ge {α : Type u_2} {P : α → Prop} {x y : α} [PartialOrder α] (hx : Minimal P x) (hy : P y) (hge : y ≤ x) :
x = y
source
theorem Minimal.eq_of_le {α : Type u_2} {P : α → Prop} {x y : α} [PartialOrder α] (hx : Minimal P x) (hy : P y) (hle : y ≤ x) :
y = x
source
theorem Maximal.eq_of_le {α : Type u_2} {P : α → Prop} {x y : α} [PartialOrder α] (hx : Maximal P x) (hy : P y) (hle : x ≤ y) :
x = y
source
theorem Maximal.eq_of_ge {α : Type u_2} {P : α → Prop} {x y : α} [PartialOrder α] (hx : Maximal P x) (hy : P y) (hge : x ≤ y) :
y = x
source
theorem minimal_iff {α : Type u_2} {P : α → Prop} {x : α} [PartialOrder α] :
Minimal P x ↔ P x ∧ ∀ ⦃y : α⦄, P y → y ≤ x → x = y
source
theorem maximal_iff {α : Type u_2} {P : α → Prop} {x : α} [PartialOrder α] :
Maximal P x ↔ P x ∧ ∀ ⦃y : α⦄, P y → x ≤ y → x = y
source
theorem minimal_mem_iff {α : Type u_2} {x : α} [PartialOrder α] {s : Set α} :
Minimal (fun (x : α) => x ∈ s) x ↔ x ∈ s ∧ ∀ ⦃y : α⦄, y ∈ s → y ≤ x → x = y
source
theorem maximal_mem_iff {α : Type u_2} {x : α} [PartialOrder α] {s : Set α} :
Maximal (fun (x : α) => x ∈ s) x ↔ x ∈ s ∧ ∀ ⦃y : α⦄, y ∈ s → x ≤ y → x = y
source
theorem minimal_iff_eq {α : Type u_2} {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`.

source
theorem maximal_iff_eq {α : Type u_2} {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`.

source
@[simp]
theorem minimal_ge_iff {α : Type u_2} {x y : α} [PartialOrder α] :
Minimal (fun (x : α) => y ≤ x) x ↔ x = y
source
@[simp]
theorem maximal_le_iff {α : Type u_2} {x y : α} [PartialOrder α] :
Maximal (fun (x : α) => x ≤ y) x ↔ x = y
source
theorem minimal_iff_minimal_of_imp_of_forall {α : Type u_2} {P Q : α → Prop} {x : α} [PartialOrder α] (hPQ : ∀ ⦃x : α⦄, Q x → P x) (h : ∀ ⦃x : α⦄, P x → ∃ y ≤ x, Q y) :
Minimal P x ↔ Minimal Q x
source
theorem maximal_iff_maximal_of_imp_of_forall {α : Type u_2} {P 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
source
theorem Minimal.eq_of_superset {α : Type u_2} {P : Set α → Prop} {s t : Set α} (h : Minimal P s) (ht : P t) (hts : t ⊆ s) :
s = t
source
theorem Maximal.eq_of_subset {α : Type u_2} {P : Set α → Prop} {s t : Set α} (h : Maximal P s) (ht : P t) (hst : s ⊆ t) :
s = t
source
theorem Minimal.eq_of_subset {α : Type u_2} {P : Set α → Prop} {s t : Set α} (h : Minimal P s) (ht : P t) (hts : t ⊆ s) :
t = s
source
theorem Maximal.eq_of_superset {α : Type u_2} {P : Set α → Prop} {s t : Set α} (h : Maximal P s) (ht : P t) (hst : s ⊆ t) :
t = s
source
theorem minimal_subset_iff {α : Type u_2} {P : Set α → Prop} {s : Set α} :
Minimal P s ↔ P s ∧ ∀ ⦃t : Set α⦄, P t → t ⊆ s → s = t
source
theorem maximal_subset_iff {α : Type u_2} {P : Set α → Prop} {s : Set α} :
Maximal P s ↔ P s ∧ ∀ ⦃t : Set α⦄, P t → s ⊆ t → s = t
source
theorem minimal_subset_iff' {α : Type u_2} {P : Set α → Prop} {s : Set α} :
Minimal P s ↔ P s ∧ ∀ ⦃t : Set α⦄, P t → t ⊆ s → s ⊆ t
source
theorem maximal_subset_iff' {α : Type u_2} {P : Set α → Prop} {s : Set α} :
Maximal P s ↔ P s ∧ ∀ ⦃t : Set α⦄, P t → s ⊆ t → t ⊆ s
source
theorem not_minimal_subset_iff {α : Type u_2} {P : Set α → Prop} {s : Set α} (hs : P s) :
¬Minimal P s ↔ ∃ t ⊂ s, P t
source
theorem not_maximal_subset_iff {α : Type u_2} {P : Set α → Prop} {s : Set α} (hs : P s) :
¬Maximal P s ↔ ∃ (t : Set α), s ⊂ t ∧ P t
source
theorem Set.minimal_iff_forall_ssubset {α : Type u_2} {P : Set α → Prop} {s : Set α} :
Minimal P s ↔ P s ∧ ∀ ⦃t : Set α⦄, t ⊂ s → ¬P t
source
theorem Minimal.not_prop_of_ssubset {α : Type u_2} {P : Set α → Prop} {s t : Set α} (h : Minimal P s) (ht : t ⊂ s) :
¬P t
source
theorem Minimal.not_ssubset {α : Type u_2} {P : Set α → Prop} {s t : Set α} (h : Minimal P s) (ht : P t) :
¬t ⊂ s
source
theorem Maximal.mem_of_prop_insert {α : Type u_2} {x : α} {P : Set α → Prop} {s : Set α} (h : Maximal P s) (hx : P (insert x s)) :
x ∈ s
source
theorem Minimal.notMem_of_prop_diff_singleton {α : Type u_2} {x : α} {P : Set α → Prop} {s : Set α} (h : Minimal P s) (hx : P (s \ {x})) :
x ∉ s
source
@[deprecated Minimal.notMem_of_prop_diff_singleton (since := "2025-05-23")]
theorem Minimal.not_mem_of_prop_diff_singleton {α : Type u_2} {x : α} {P : Set α → Prop} {s : Set α} (h : Minimal P s) (hx : P (s \ {x})) :
x ∉ s

Alias of `Minimal.notMem_of_prop_diff_singleton`.

source
theorem Set.minimal_iff_forall_diff_singleton {α : Type u_2} {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})
source
theorem Set.exists_diff_singleton_of_not_minimal {α : Type u_2} {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})
source
theorem Set.maximal_iff_forall_ssuperset {α : Type u_2} {P : Set α → Prop} {s : Set α} :
Maximal P s ↔ P s ∧ ∀ ⦃t : Set α⦄, s ⊂ t → ¬P t
source
theorem Maximal.not_prop_of_ssuperset {α : Type u_2} {P : Set α → Prop} {s t : Set α} (h : Maximal P s) (ht : s ⊂ t) :
¬P t
source
theorem Maximal.not_ssuperset {α : Type u_2} {P : Set α → Prop} {s t : Set α} (h : Maximal P s) (ht : P t) :
¬s ⊂ t
source
theorem Set.maximal_iff_forall_insert {α : Type u_2} {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)
source
theorem Set.exists_insert_of_not_maximal {α : Type u_2} {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)
source
theorem setOf_minimal_subset {α : Type u_2} [Preorder α] (s : Set α) :
{x : α | Minimal (fun (x : α) => x ∈ s) x} ⊆ s
source
theorem setOf_maximal_subset {α : Type u_2} [Preorder α] (s : Set α) :
{x : α | Maximal (fun (x : α) => x ∈ s) x} ⊆ s
source
theorem Set.Subsingleton.maximal_mem_iff {α : Type u_2} {x : α} {s : Set α} [Preorder α] (h : s.Subsingleton) :
Maximal (fun (x : α) => x ∈ s) x ↔ x ∈ s
source
theorem Set.Subsingleton.minimal_mem_iff {α : Type u_2} {x : α} {s : Set α} [Preorder α] (h : s.Subsingleton) :
Minimal (fun (x : α) => x ∈ s) x ↔ x ∈ s
source
theorem IsLeast.minimal {α : Type u_2} {x : α} {s : Set α} [Preorder α] (h : IsLeast s x) :
Minimal (fun (x : α) => x ∈ s) x
source
theorem IsGreatest.maximal {α : Type u_2} {x : α} {s : Set α} [Preorder α] (h : IsGreatest s x) :
Maximal (fun (x : α) => x ∈ s) x
source
theorem IsLeast.minimal_iff {α : Type u_2} {a x : α} {s : Set α} [PartialOrder α] (h : IsLeast s a) :
Minimal (fun (x : α) => x ∈ s) x ↔ x = a
source
theorem IsGreatest.maximal_iff {α : Type u_2} {a x : α} {s : Set α} [PartialOrder α] (h : IsGreatest s a) :
Maximal (fun (x : α) => x ∈ s) x ↔ x = a
source
theorem minimal_mem_image_monotone {α : Type u_2} {x : α} [Preorder α] {β : Type u_3} [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)
source
theorem maximal_mem_image_monotone {α : Type u_2} {x : α} [Preorder α] {β : Type u_3} [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)
source
theorem minimal_mem_image_monotone_iff {α : Type u_2} {a : α} [Preorder α] {β : Type u_3} [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
source
theorem maximal_mem_image_monotone_iff {α : Type u_2} {a : α} [Preorder α] {β : Type u_3} [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
source
theorem minimal_mem_image_antitone {α : Type u_2} {x : α} [Preorder α] {β : Type u_3} [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)
source
theorem maximal_mem_image_antitone {α : Type u_2} {x : α} [Preorder α] {β : Type u_3} [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)
source
theorem minimal_mem_image_antitone_iff {α : Type u_2} {a : α} [Preorder α] {β : Type u_3} [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
source
theorem maximal_mem_image_antitone_iff {α : Type u_2} {a : α} [Preorder α] {β : Type u_3} [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
source
theorem image_monotone_setOf_minimal {α : Type u_2} {P : α → Prop} [Preorder α] {β : Type u_3} [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}
source
theorem image_monotone_setOf_maximal {α : Type u_2} {P : α → Prop} [Preorder α] {β : Type u_3} [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}
source
theorem image_antitone_setOf_minimal {α : Type u_2} {P : α → Prop} [Preorder α] {β : Type u_3} [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}
source
theorem image_antitone_setOf_maximal {α : Type u_2} {P : α → Prop} [Preorder α] {β : Type u_3} [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}
source
theorem image_monotone_setOf_minimal_mem {α : Type u_2} [Preorder α] {β : Type u_3} [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}
source
theorem image_monotone_setOf_maximal_mem {α : Type u_2} [Preorder α] {β : Type u_3} [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}
source
theorem image_antitone_setOf_minimal_mem {α : Type u_2} [Preorder α] {β : Type u_3} [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}
source
theorem image_antitone_setOf_maximal_mem {α : Type u_2} [Preorder α] {β : Type u_3} [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}
source
theorem OrderEmbedding.minimal_mem_image {α : Type u_2} {x : α} [Preorder α] {β : Type u_3} [Preorder β] {s : Set α} (f : α ↪o β) (hx : Minimal (fun (x : α) => x ∈ s) x) :
Minimal (fun (x : β) => x ∈ ⇑f '' s) (f x)
source
theorem OrderEmbedding.maximal_mem_image {α : Type u_2} {x : α} [Preorder α] {β : Type u_3} [Preorder β] {s : Set α} (f : α ↪o β) (hx : Maximal (fun (x : α) => x ∈ s) x) :
Maximal (fun (x : β) => x ∈ ⇑f '' s) (f x)
source
theorem OrderEmbedding.minimal_mem_image_iff {α : Type u_2} {a : α} [Preorder α] {β : Type u_3} [Preorder β] {s : Set α} {f : α ↪o β} (ha : a ∈ s) :
Minimal (fun (x : β) => x ∈ ⇑f '' s) (f a) ↔ Minimal (fun (x : α) => x ∈ s) a
source
theorem OrderEmbedding.maximal_mem_image_iff {α : Type u_2} {a : α} [Preorder α] {β : Type u_3} [Preorder β] {s : Set α} {f : α ↪o β} (ha : a ∈ s) :
Maximal (fun (x : β) => x ∈ ⇑f '' s) (f a) ↔ Maximal (fun (x : α) => x ∈ s) a
source
theorem OrderEmbedding.minimal_apply_mem_inter_range_iff {α : Type u_2} {x : α} [Preorder α] {β : Type u_3} [Preorder β] {f : α ↪o β} {t : Set β} :
Minimal (fun (x : β) => x ∈ t ∩ Set.range ⇑f) (f x) ↔ Minimal (fun (x : α) => f x ∈ t) x
source
theorem OrderEmbedding.maximal_apply_mem_inter_range_iff {α : Type u_2} {x : α} [Preorder α] {β : Type u_3} [Preorder β] {f : α ↪o β} {t : Set β} :
Maximal (fun (x : β) => x ∈ t ∩ Set.range ⇑f) (f x) ↔ Maximal (fun (x : α) => f x ∈ t) x
source
theorem OrderEmbedding.minimal_apply_mem_iff {α : Type u_2} {x : α} [Preorder α] {β : Type u_3} [Preorder β] {f : α ↪o β} {t : Set β} (ht : t ⊆ Set.range ⇑f) :
Minimal (fun (x : β) => x ∈ t) (f x) ↔ Minimal (fun (x : α) => f x ∈ t) x
source
theorem OrderEmbedding.maximal_apply_iff {α : Type u_2} {x : α} [Preorder α] {β : Type u_3} [Preorder β] {f : α ↪o β} {t : Set β} (ht : t ⊆ Set.range ⇑f) :
Maximal (fun (x : β) => x ∈ t) (f x) ↔ Maximal (fun (x : α) => f x ∈ t) x
source
@[simp]
theorem OrderEmbedding.image_setOf_minimal {α : Type u_2} [Preorder α] {β : Type u_3} [Preorder β] {s : Set α} {f : α ↪o β} :
⇑f '' {x : α | Minimal (fun (x : α) => x ∈ s) x} = {x : β | Minimal (fun (x : β) => x ∈ ⇑f '' s) x}
source
@[simp]
theorem OrderEmbedding.image_setOf_maximal {α : Type u_2} [Preorder α] {β : Type u_3} [Preorder β] {s : Set α} {f : α ↪o β} :
⇑f '' {x : α | Maximal (fun (x : α) => x ∈ s) x} = {x : β | Maximal (fun (x : β) => x ∈ ⇑f '' s) x}
source
theorem OrderEmbedding.inter_preimage_setOf_minimal_eq_of_subset {α : Type u_2} {x : α} [Preorder α] {β : Type u_3} [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
source
theorem OrderEmbedding.inter_preimage_setOf_maximal_eq_of_subset {α : Type u_2} {x : α} [Preorder α] {β : Type u_3} [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
source
theorem OrderIso.image_setOf_minimal {α : Type u_2} [Preorder α] {β : Type u_3} [Preorder β] (f : α ≃o β) (P : α → Prop) :
⇑f '' {x : α | Minimal P x} = {x : β | Minimal (fun (x : β) => P (f.symm x)) x}
source
theorem OrderIso.image_setOf_maximal {α : Type u_2} [Preorder α] {β : Type u_3} [Preorder β] (f : α ≃o β) (P : α → Prop) :
⇑f '' {x : α | Maximal P x} = {x : β | Maximal (fun (x : β) => P (f.symm x)) x}
source
theorem OrderIso.map_minimal_mem {α : Type u_2} {x : α} [Preorder α] {β : Type u_3} [Preorder β] {s : Set α} {t : Set β} (f : ↑s ≃o ↑t) (hx : Minimal (fun (x : α) => x ∈ s) x) :
Minimal (fun (x : β) => x ∈ t) ↑(f ⟨x, ⋯⟩)
source
theorem OrderIso.map_maximal_mem {α : Type u_2} {x : α} [Preorder α] {β : Type u_3} [Preorder β] {s : Set α} {t : Set β} (f : ↑s ≃o ↑t) (hx : Maximal (fun (x : α) => x ∈ s) x) :
Maximal (fun (x : β) => x ∈ t) ↑(f ⟨x, ⋯⟩)
source
def OrderIso.mapSetOfMinimal {α : Type u_2} [Preorder α] {β : Type u_3} [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

source
def OrderIso.mapSetOfMaximal {α : Type u_2} [Preorder α] {β : Type u_3} [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

source
def OrderIso.setOfMinimalIsoSetOfMaximal {α : Type u_2} [Preorder α] {β : Type u_3} [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

source
def OrderIso.setOfMaximalIsoSetOfMinimal {α : Type u_2} [Preorder α] {β : Type u_3} [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

source
theorem minimal_mem_Icc {α : Type u_2} {x : α} [PartialOrder α] {a b : α} (hab : a ≤ b) :
Minimal (fun (x : α) => x ∈ Set.Icc a b) x ↔ x = a
source
theorem maximal_mem_Icc {α : Type u_2} {x : α} [PartialOrder α] {a b : α} (hab : a ≤ b) :
Maximal (fun (x : α) => x ∈ Set.Icc a b) x ↔ x = b
source
theorem minimal_mem_Ico {α : Type u_2} {x : α} [PartialOrder α] {a b : α} (hab : a < b) :
Minimal (fun (x : α) => x ∈ Set.Ico a b) x ↔ x = a
source
theorem maximal_mem_Ioc {α : Type u_2} {x : α} [PartialOrder α] {a b : α} (hab : a < b) :
Maximal (fun (x : α) => x ∈ Set.Ioc a b) x ↔ x = b