Documentation

Mathlib.Order.Minimal

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

@[simp]

theorem minimalFor_eq_iff {ι : Type u_1} {α : Type u_2} [LE α] {f : ι → α} {i j : ι} :

MinimalFor (fun (x : ι) => x = j) f i ↔ i = j

@[simp]

theorem maximalFor_eq_iff {ι : Type u_1} {α : Type u_2} [LE α] {f : ι → α} {i j : ι} :

MaximalFor (fun (x : ι) => x = j) f i ↔ i = j

@[simp]

theorem minimalFor_id {α : Type u_2} {P : α → Prop} {x : α} [LE α] :

MinimalFor P id x ↔ Minimal P x

@[simp]

theorem maximalFor_id {α : Type u_2} {P : α → Prop} {x : α} [LE α] :

MaximalFor P id x ↔ Maximal P x

@[simp]

theorem minimal_toDual {α : Type u_2} {P : α → Prop} {x : α} [LE α] :

Minimal (fun (x : αᵒᵈ) => P (OrderDual.ofDual x)) (OrderDual.toDual x) ↔ Maximal P x

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.

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.

@[simp]

theorem maximal_toDual {α : Type u_2} {P : α → Prop} {x : α} [LE α] :

Maximal (fun (x : αᵒᵈ) => P (OrderDual.ofDual x)) (OrderDual.toDual x) ↔ Minimal P x

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.

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.

@[simp]

theorem minimal_false {α : Type u_2} {x : α} [LE α] :

¬Minimal (fun (x : α) => False) x

@[simp]

theorem maximal_false {α : Type u_2} {x : α} [LE α] :

¬Maximal (fun (x : α) => False) x

@[simp]

theorem minimal_true {α : Type u_2} {x : α} [LE α] :

Minimal (fun (x : α) => True) x ↔ IsMin x

@[simp]

theorem maximal_true {α : Type u_2} {x : α} [LE α] :

Maximal (fun (x : α) => True) x ↔ IsMax x

@[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

@[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

theorem maximal_true_subtype {α : Type u_2} {P : α → Prop} [LE α] {x : Subtype P} :

Maximal (fun (x : Subtype P) => True) x ↔ Maximal P ↑x

theorem minimal_true_subtype {α : Type u_2} {P : α → Prop} [LE α] {x : Subtype P} :

Minimal (fun (x : Subtype P) => True) x ↔ Minimal P ↑x

@[simp]

theorem minimal_minimal {α : Type u_2} {P : α → Prop} {x : α} [LE α] :

Minimal (Minimal P) x ↔ Minimal P x

@[simp]

theorem maximal_maximal {α : Type u_2} {P : α → Prop} {x : α} [LE α] :

Maximal (Maximal P) x ↔ Maximal P x

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.

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.

theorem Minimal.mono {α : Type u_2} {P Q : α → Prop} {x : α} [LE α] (h : Minimal P x) (hle : Q ≤ P) (hQ : Q x) :

theorem Maximal.mono {α : Type u_2} {P Q : α → Prop} {x : α} [LE α] (h : Maximal P x) (hle : Q ≤ P) (hQ : Q x) :

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

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

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

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

@[simp]

theorem minimal_eq_iff {α : Type u_2} {x y : α} [LE α] :

Minimal (fun (x : α) => x = y) x ↔ x = y

@[simp]

theorem maximal_eq_iff {α : Type u_2} {x y : α} [LE α] :

Maximal (fun (x : α) => x = y) x ↔ x = y

theorem not_minimal_iff {α : Type u_2} {P : α → Prop} {x : α} [LE α] (hx : P x) :

¬Minimal P x ↔ ∃ (y : α), P y ∧ y ≤ x ∧ ¬x ≤ y

theorem not_maximal_iff {α : Type u_2} {P : α → Prop} {x : α} [LE α] (hx : P x) :

¬Maximal P x ↔ ∃ (y : α), P y ∧ x ≤ y ∧ ¬y ≤ x

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

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

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

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

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

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

theorem minimal_iff_forall_lt {α : Type u_2} {P : α → Prop} {x : α} [Preorder α] :

Minimal P x ↔ P x ∧ ∀ ⦃y : α⦄, y < x → ¬P y

theorem maximal_iff_forall_gt {α : Type u_2} {P : α → Prop} {x : α} [Preorder α] :

Maximal P x ↔ P x ∧ ∀ ⦃y : α⦄, x < y → ¬P y

theorem Minimal.not_prop_of_lt {α : Type u_2} {P : α → Prop} {x y : α} [Preorder α] (h : Minimal P x) (hlt : y < x) :

¬P y

theorem Maximal.not_prop_of_gt {α : Type u_2} {P : α → Prop} {x y : α} [Preorder α] (h : Maximal P x) (hlt : x < y) :

¬P y

theorem Minimal.not_lt {α : Type u_2} {P : α → Prop} {x y : α} [Preorder α] (h : Minimal P x) (hy : P y) :

¬y < x

theorem Maximal.not_gt {α : Type u_2} {P : α → Prop} {x y : α} [Preorder α] (h : Maximal P x) (hy : P y) :

¬x < y

@[simp]

theorem minimal_le_iff {α : Type u_2} {x y : α} [Preorder α] :

Minimal (fun (x : α) => x ≤ y) x ↔ x ≤ y ∧ IsMin x

@[simp]

theorem maximal_ge_iff {α : Type u_2} {x y : α} [Preorder α] :

Maximal (fun (x : α) => y ≤ x) x ↔ y ≤ x ∧ IsMax x

@[simp]

theorem minimal_lt_iff {α : Type u_2} {x y : α} [Preorder α] :

Minimal (fun (x : α) => x < y) x ↔ x < y ∧ IsMin x

@[simp]

theorem maximal_gt_iff {α : Type u_2} {x y : α} [Preorder α] :

Maximal (fun (x : α) => y < x) x ↔ y < x ∧ IsMax x

theorem not_minimal_iff_exists_lt {α : Type u_2} {P : α → Prop} {x : α} [Preorder α] (hx : P x) :

¬Minimal P x ↔ ∃ (y : α), y < x ∧ P y

theorem exists_lt_of_not_minimal {α : Type u_2} {P : α → Prop} {x : α} [Preorder α] (hx : P x) :

¬Minimal P x → ∃ (y : α), y < x ∧ P y

Alias of the forward direction of not_minimal_iff_exists_lt.

theorem not_maximal_iff_exists_gt {α : Type u_2} {P : α → Prop} {x : α} [Preorder α] (hx : P x) :

¬Maximal P x ↔ ∃ (y : α), x < y ∧ P y

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.

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

theorem exists_minimal_of_wellFoundedLT {α : Type u_2} [Preorder α] [WellFoundedLT α] (P : α → Prop) (hP : ∃ (a : α), P a) :

∃ (a : α), Minimal P a

theorem exists_minimal_le_of_wellFoundedLT {α : Type u_2} [Preorder α] [WellFoundedLT α] (P : α → Prop) (a : α) (ha : P a) :

∃ (b : α), b ≤ a ∧ Minimal P b

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

theorem exists_maximal_of_wellFoundedGT {α : Type u_2} [Preorder α] [WellFoundedGT α] (P : α → Prop) (hP : ∃ (a : α), P a) :

∃ (a : α), Maximal P a

theorem exists_maximal_ge_of_wellFoundedGT {α : Type u_2} [Preorder α] [WellFoundedGT α] (P : α → Prop) (a : α) (ha : P a) :

∃ (b : α), a ≤ b ∧ Maximal P b

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

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

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

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

theorem minimal_iff {α : Type u_2} {P : α → Prop} {x : α} [PartialOrder α] :

Minimal P x ↔ P x ∧ ∀ ⦃y : α⦄, P y → y ≤ x → x = y

theorem maximal_iff {α : Type u_2} {P : α → Prop} {x : α} [PartialOrder α] :

Maximal P x ↔ P x ∧ ∀ ⦃y : α⦄, P y → x ≤ y → x = y

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

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

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.

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.

@[simp]

theorem minimal_ge_iff {α : Type u_2} {x y : α} [PartialOrder α] :

Minimal (fun (x : α) => y ≤ x) x ↔ x = y

@[simp]

theorem maximal_le_iff {α : Type u_2} {x y : α} [PartialOrder α] :

Maximal (fun (x : α) => x ≤ y) x ↔ x = y

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 : α), y ≤ x ∧ Q y) :

Minimal P x ↔ Minimal Q x

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

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

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

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

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

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

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

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

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

theorem not_minimal_subset_iff {α : Type u_2} {P : Set α → Prop} {s : Set α} (hs : P s) :

¬Minimal P s ↔ ∃ (t : Set α), t ⊂ s ∧ P t

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

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

theorem Minimal.not_prop_of_ssubset {α : Type u_2} {P : Set α → Prop} {s t : Set α} (h : Minimal P s) (ht : t ⊂ s) :

¬P t

theorem Minimal.not_ssubset {α : Type u_2} {P : Set α → Prop} {s t : Set α} (h : Minimal P s) (ht : P t) :

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

theorem Minimal.notMem_of_prop_diff_singleton {α : Type u_2} {x : α} {P : Set α → Prop} {s : Set α} (h : Minimal P s) (hx : P (s \ {x})) :

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 : α), x ∈ s → ¬P (s \ {x})

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 : α), x ∈ s ∧ P (s \ {x})

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

theorem Maximal.not_prop_of_ssuperset {α : Type u_2} {P : Set α → Prop} {s t : Set α} (h : Maximal P s) (ht : s ⊂ t) :

¬P t

theorem Maximal.not_ssuperset {α : Type u_2} {P : Set α → Prop} {s t : Set α} (h : Maximal P s) (ht : P t) :

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 : α), ¬x ∈ s → ¬P (insert x s)

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 : α), ¬x ∈ s ∧ P (insert x s)

theorem setOf_minimal_subset {α : Type u_2} [Preorder α] (s : Set α) :

{x : α | Minimal (fun (x : α) => x ∈ s) x} ⊆ s

theorem setOf_maximal_subset {α : Type u_2} [Preorder α] (s : Set α) :

{x : α | Maximal (fun (x : α) => x ∈ s) x} ⊆ s

theorem Set.Subsingleton.maximal_mem_iff {α : Type u_2} {x : α} {s : Set α} [Preorder α] (h : s.Subsingleton) :

Maximal (fun (x : α) => x ∈ s) x ↔ x ∈ s

theorem Set.Subsingleton.minimal_mem_iff {α : Type u_2} {x : α} {s : Set α} [Preorder α] (h : s.Subsingleton) :

Minimal (fun (x : α) => x ∈ s) x ↔ x ∈ s

theorem IsLeast.minimal {α : Type u_2} {x : α} {s : Set α} [Preorder α] (h : IsLeast s x) :

Minimal (fun (x : α) => x ∈ s) x

theorem IsGreatest.maximal {α : Type u_2} {x : α} {s : Set α} [Preorder α] (h : IsGreatest s x) :

Maximal (fun (x : α) => x ∈ s) x

theorem IsLeast.minimal_iff {α : Type u_2} {a x : α} {s : Set α} [PartialOrder α] (h : IsLeast s a) :

Minimal (fun (x : α) => x ∈ s) x ↔ x = a

theorem IsGreatest.maximal_iff {α : Type u_2} {a x : α} {s : Set α} [PartialOrder α] (h : IsGreatest s a) :

Maximal (fun (x : α) => x ∈ s) x ↔ x = a

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)

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)

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

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

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)

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)

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

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

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}

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}

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}

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}

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}

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}

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}

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}

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)

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)

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

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

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

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

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

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

@[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}

@[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}

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

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

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}

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}

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, ⋯⟩)

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, ⋯⟩)

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

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

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

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

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

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

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

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