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_sdiff_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

theorem MinimalFor.anti {ι : Type u_1} {α : Type u_2} [LE α] {P Q : ι → Prop} {f : ι → α} {i : ι} (h : MinimalFor P f i) (hle : Q ≤ P) (hQ : Q i) : MinimalFor Q f i

theorem MaximalFor.anti {ι : Type u_1} {α : Type u_2} [LE α] {P Q : ι → Prop} {f : ι → α} {i : ι} (h : MaximalFor P f i) (hle : Q ≤ P) (hQ : Q i) : MaximalFor Q f i

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

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

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 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 minimal_true_subtype {α : Type u_2} {P : α → Prop} [LE α] {x : Subtype P} : Minimal (fun (x : Subtype P) => True) x ↔ Minimal P ↑x

theorem maximal_true_subtype {α : Type u_2} {P : α → Prop} [LE α] {x : Subtype P} : Maximal (fun (x : Subtype P) => True) x ↔ Maximal 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) : Minimal Q x

theorem Maximal.mono {α : Type u_2} {P Q : α → Prop} {x : α} [LE α] (h : Maximal P x) (hle : Q ≤ P) (hQ : Q x) : Maximal 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 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 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_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 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 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_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 minimalFor_iff_forall_lt {ι : Type u_1} {α : Type u_2} [Preorder α] {Q : ι → Prop} {f : ι → α} {i : ι} : MinimalFor Q f i ↔ Q i ∧ ∀ ⦃j : ι⦄, f j < f i → ¬Q j

theorem maximalFor_iff_forall_gt {ι : Type u_1} {α : Type u_2} [Preorder α] {Q : ι → Prop} {f : ι → α} {i : ι} : MaximalFor Q f i ↔ Q i ∧ ∀ ⦃j : ι⦄, f i < f j → ¬Q j

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 MinimalFor.not_prop_of_lt {ι : Type u_1} {α : Type u_2} [Preorder α] {Q : ι → Prop} {f : ι → α} {i j : ι} (h : MinimalFor Q f i) (hlt : f j < f i) : ¬Q j

theorem MaximalFor.not_prop_of_gt {ι : Type u_1} {α : Type u_2} [Preorder α] {Q : ι → Prop} {f : ι → α} {i j : ι} (h : MaximalFor Q f i) (hlt : f i < f j) : ¬Q j

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

theorem MinimalFor.not_lt {ι : Type u_1} {α : Type u_2} [Preorder α] {Q : ι → Prop} {f : ι → α} {i j : ι} (h : MinimalFor Q f i) (hj : Q j) : ¬f j < f i

theorem MaximalFor.not_gt {ι : Type u_1} {α : Type u_2} [Preorder α] {Q : ι → Prop} {f : ι → α} {i j : ι} (h : MaximalFor Q f i) (hj : Q j) : ¬f i < f j

@[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 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_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 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 MinimalFor.of_strictMonoOn_comp {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {Q : ι → Prop} {f : ι → α} {g : α → β} {i : ι} (hg : StrictMonoOn g (f '' Set.ofPred Q)) (h : MinimalFor Q (g ∘ f) i) : MinimalFor Q f i

theorem MaximalFor.of_strictMonoOn_comp {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {Q : ι → Prop} {f : ι → α} {g : α → β} {i : ι} (hg : StrictMonoOn g (f '' Set.ofPred Q)) (h : MaximalFor Q (g ∘ f) i) : MaximalFor Q f i

theorem MinimalFor.minimal_of_strictMonoOn {α : Type u_2} {β : Type u_3} {P : α → Prop} {x : α} [Preorder α] [Preorder β] {g : α → β} (hg : StrictMonoOn g (Set.ofPred P)) (h : MinimalFor P g x) : Minimal P x

theorem MaximalFor.maximal_of_strictMonoOn {α : Type u_2} {β : Type u_3} {P : α → Prop} {x : α} [Preorder α] [Preorder β] {g : α → β} (hg : StrictMonoOn g (Set.ofPred P)) (h : MaximalFor P g x) : Maximal P x

theorem MinimalFor.maximalFor_of_strictAntiOn_comp {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {Q : ι → Prop} {f : ι → α} {g : α → β} {i : ι} (hg : StrictAntiOn g (f '' Set.ofPred Q)) (h : MinimalFor Q (g ∘ f) i) : MaximalFor Q f i

theorem MaximalFor.minimalFor_of_strictAntiOn_comp {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {Q : ι → Prop} {f : ι → α} {g : α → β} {i : ι} (hg : StrictAntiOn g (f '' Set.ofPred Q)) (h : MaximalFor Q (g ∘ f) i) : MinimalFor Q f i

theorem MinimalFor.maximal_of_strictAntiOn {α : Type u_2} {β : Type u_3} {P : α → Prop} {x : α} [Preorder α] [Preorder β] {g : α → β} (hg : StrictAntiOn g (Set.ofPred P)) (h : MinimalFor P g x) : Maximal P x

theorem MaximalFor.minimal_of_strictAntiOn {α : Type u_2} {β : Type u_3} {P : α → Prop} {x : α} [Preorder α] [Preorder β] {g : α → β} (hg : StrictAntiOn g (Set.ofPred P)) (h : MaximalFor P g x) : Minimal P x

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_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_minimal_of_wellFoundedLT {α : Type u_2} [Preorder α] [WellFoundedLT α] (P : α → Prop) (hP : ∃ (a : α), P a) : ∃ (a : α), Minimal P a

theorem exists_maximal_of_wellFoundedGT {α : Type u_2} [Preorder α] [WellFoundedGT α] (P : α → Prop) (hP : ∃ (a : α), P a) : ∃ (a : α), Maximal 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_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 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 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_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.le {α : Type u_2} {P : α → Prop} {x y : α} [LinearOrder α] (h : Minimal P x) (hy : P y) : x ≤ y

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

theorem MinimalFor.le {ι : Type u_1} {α : Type u_2} [LinearOrder α] {i j : ι} {Q : ι → Prop} {f : ι → α} (h : MinimalFor Q f i) (hj : Q j) : f i ≤ f j

theorem MaximalFor.le {ι : Type u_1} {α : Type u_2} [LinearOrder α] {i j : ι} {Q : ι → Prop} {f : ι → α} (h : MaximalFor Q f i) (hj : Q j) : f j ≤ f i

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) : ¬t ⊂ s

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_sdiff_singleton {α : Type u_2} {x : α} {P : Set α → Prop} {s : Set α} (h : Minimal P s) (hx : P (s \ {x})) : ¬x ∈ s

@[deprecated Minimal.notMem_of_prop_sdiff_singleton (since := "2026-06-03")]

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

Alias of Minimal.notMem_of_prop_sdiff_singleton.

theorem Set.minimal_iff_forall_sdiff_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})

@[deprecated Set.minimal_iff_forall_sdiff_singleton (since := "2026-06-03")]

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})

Alias of Set.minimal_iff_forall_sdiff_singleton.

theorem Set.exists_sdiff_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})

@[deprecated Set.exists_sdiff_singleton_of_not_minimal (since := "2026-06-03")]

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})

Alias of Set.exists_sdiff_singleton_of_not_minimal.

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) : ¬s ⊂ 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 setOfPred_minimal_subset {α : Type u_2} [Preorder α] (s : Set α) : {x : α | Minimal (fun (x : α) => x ∈ s) x} ⊆ s

theorem setOfPred_maximal_subset {α : Type u_2} [Preorder α] (s : Set α) : {x : α | Maximal (fun (x : α) => x ∈ s) x} ⊆ s

@[deprecated setOfPred_minimal_subset (since := "2026-07-09")]

theorem setOf_minimal_subset {α : Type u_2} [Preorder α] (s : Set α) : {x : α | Minimal (fun (x : α) => x ∈ s) x} ⊆ s

Alias of setOfPred_minimal_subset.

@[deprecated setOfPred_maximal_subset (since := "2026-07-09")]

theorem setOf_maximal_subset {α : Type u_2} [Preorder α] (s : Set α) : {x : α | Maximal (fun (x : α) => x ∈ s) x} ⊆ s

Alias of setOfPred_maximal_subset.

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 Set.Subsingleton.maximal_mem_iff {α : Type u_2} {x : α} {s : Set α} [Preorder α] (h : s.Subsingleton) : Maximal (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} {β : Type u_3} {x : α} [Preorder α] [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} {β : Type u_3} {x : α} [Preorder α] [Preorder β] {s : Set α} {f : α → β} (hf : ∀ ⦃y x : α⦄, y ∈ s → x ∈ s → (f y ≤ f x ↔ y ≤ x)) (hx : Maximal (fun (x : α) => x ∈ s) x) : Maximal (fun (x : β) => x ∈ f '' s) (f x)

theorem minimal_mem_image_monotone_iff {α : Type u_2} {β : Type u_3} {a : α} [Preorder α] [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} {β : Type u_3} {a : α} [Preorder α] [Preorder β] {s : Set α} {f : α → β} (ha : a ∈ s) (hf : ∀ ⦃y x : α⦄, y ∈ s → x ∈ s → (f y ≤ f x ↔ y ≤ x)) : Maximal (fun (x : β) => x ∈ f '' s) (f a) ↔ Maximal (fun (x : α) => x ∈ s) a

theorem minimal_mem_image_antitone {α : Type u_2} {β : Type u_3} {x : α} [Preorder α] [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} {β : Type u_3} {x : α} [Preorder α] [Preorder β] {s : Set α} {f : α → β} (hf : ∀ ⦃y x : α⦄, y ∈ s → x ∈ s → (f y ≤ f x ↔ x ≤ y)) (hx : Maximal (fun (x : α) => x ∈ s) x) : Minimal (fun (x : β) => x ∈ f '' s) (f x)

theorem minimal_mem_image_antitone_iff {α : Type u_2} {β : Type u_3} {a : α} [Preorder α] [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} {β : Type u_3} {a : α} [Preorder α] [Preorder β] {s : Set α} {f : α → β} (ha : a ∈ s) (hf : ∀ ⦃y x : α⦄, y ∈ s → x ∈ s → (f y ≤ f x ↔ x ≤ y)) : Maximal (fun (x : β) => x ∈ f '' s) (f a) ↔ Minimal (fun (x : α) => x ∈ s) a

theorem image_monotone_setOfPred_minimal {α : Type u_2} {β : Type u_3} {P : α → Prop} [Preorder α] [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_setOfPred_maximal {α : Type u_2} {β : Type u_3} {P : α → Prop} [Preorder α] [Preorder β] {f : α → β} (hf : ∀ ⦃y x : α⦄, P y → P x → (f y ≤ f x ↔ y ≤ x)) : f '' {x : α | Maximal P x} = {x : β | Maximal (fun (x : β) => ∃ (x₀ : α), P x₀ ∧ f x₀ = x) x}

@[deprecated image_monotone_setOfPred_minimal (since := "2026-07-09")]

theorem image_monotone_setOf_minimal {α : Type u_2} {β : Type u_3} {P : α → Prop} [Preorder α] [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}

Alias of image_monotone_setOfPred_minimal.

@[deprecated image_monotone_setOfPred_maximal (since := "2026-07-09")]

theorem image_monotone_setOf_maximal {α : Type u_2} {β : Type u_3} {P : α → Prop} [Preorder α] [Preorder β] {f : α → β} (hf : ∀ ⦃y x : α⦄, P y → P x → (f y ≤ f x ↔ y ≤ x)) : f '' {x : α | Maximal P x} = {x : β | Maximal (fun (x : β) => ∃ (x₀ : α), P x₀ ∧ f x₀ = x) x}

Alias of image_monotone_setOfPred_maximal.

theorem image_antitone_setOfPred_minimal {α : Type u_2} {β : Type u_3} {P : α → Prop} [Preorder α] [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_setOfPred_maximal {α : Type u_2} {β : Type u_3} {P : α → Prop} [Preorder α] [Preorder β] {f : α → β} (hf : ∀ ⦃y x : α⦄, P y → P x → (f y ≤ f x ↔ x ≤ y)) : f '' {x : α | Maximal P x} = {x : β | Minimal (fun (x : β) => ∃ (x₀ : α), P x₀ ∧ f x₀ = x) x}

@[deprecated image_antitone_setOfPred_minimal (since := "2026-07-09")]

theorem image_antitone_setOf_minimal {α : Type u_2} {β : Type u_3} {P : α → Prop} [Preorder α] [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}

Alias of image_antitone_setOfPred_minimal.

@[deprecated image_antitone_setOfPred_maximal (since := "2026-07-09")]

theorem image_antitone_setOf_maximal {α : Type u_2} {β : Type u_3} {P : α → Prop} [Preorder α] [Preorder β] {f : α → β} (hf : ∀ ⦃y x : α⦄, P y → P x → (f y ≤ f x ↔ x ≤ y)) : f '' {x : α | Maximal P x} = {x : β | Minimal (fun (x : β) => ∃ (x₀ : α), P x₀ ∧ f x₀ = x) x}

Alias of image_antitone_setOfPred_maximal.

theorem image_monotone_setOfPred_minimal_mem {α : Type u_2} {β : Type u_3} [Preorder α] [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_setOfPred_maximal_mem {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {s : Set α} {f : α → β} (hf : ∀ ⦃y x : α⦄, y ∈ s → x ∈ s → (f y ≤ f x ↔ y ≤ x)) : f '' {x : α | Maximal (fun (x : α) => x ∈ s) x} = {x : β | Maximal (fun (x : β) => x ∈ f '' s) x}

@[deprecated image_monotone_setOfPred_minimal_mem (since := "2026-07-09")]

theorem image_monotone_setOf_minimal_mem {α : Type u_2} {β : Type u_3} [Preorder α] [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}

Alias of image_monotone_setOfPred_minimal_mem.

@[deprecated image_monotone_setOfPred_maximal_mem (since := "2026-07-09")]

theorem image_monotone_setOf_maximal_mem {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {s : Set α} {f : α → β} (hf : ∀ ⦃y x : α⦄, y ∈ s → x ∈ s → (f y ≤ f x ↔ y ≤ x)) : f '' {x : α | Maximal (fun (x : α) => x ∈ s) x} = {x : β | Maximal (fun (x : β) => x ∈ f '' s) x}

Alias of image_monotone_setOfPred_maximal_mem.

theorem image_antitone_setOfPred_minimal_mem {α : Type u_2} {β : Type u_3} [Preorder α] [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_setOfPred_maximal_mem {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {s : Set α} {f : α → β} (hf : ∀ ⦃y x : α⦄, y ∈ s → x ∈ s → (f y ≤ f x ↔ x ≤ y)) : f '' {x : α | Maximal (fun (x : α) => x ∈ s) x} = {x : β | Minimal (fun (x : β) => x ∈ f '' s) x}

@[deprecated image_antitone_setOfPred_minimal_mem (since := "2026-07-09")]

theorem image_antitone_setOf_minimal_mem {α : Type u_2} {β : Type u_3} [Preorder α] [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}

Alias of image_antitone_setOfPred_minimal_mem.

@[deprecated image_antitone_setOfPred_maximal_mem (since := "2026-07-09")]

theorem image_antitone_setOf_maximal_mem {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {s : Set α} {f : α → β} (hf : ∀ ⦃y x : α⦄, y ∈ s → x ∈ s → (f y ≤ f x ↔ x ≤ y)) : f '' {x : α | Maximal (fun (x : α) => x ∈ s) x} = {x : β | Minimal (fun (x : β) => x ∈ f '' s) x}

Alias of image_antitone_setOfPred_maximal_mem.

theorem OrderEmbedding.minimal_mem_image {α : Type u_2} {β : Type u_3} {x : α} [Preorder α] [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} {β : Type u_3} {x : α} [Preorder α] [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} {β : Type u_3} {a : α} [Preorder α] [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} {β : Type u_3} {a : α} [Preorder α] [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} {β : Type u_3} {x : α} [Preorder α] [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} {β : Type u_3} {x : α} [Preorder α] [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} {β : Type u_3} {x : α} [Preorder α] [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_mem_iff {α : Type u_2} {β : Type u_3} {x : α} [Preorder α] [Preorder β] {f : α ↪o β} {t : Set β} (ht : t ⊆ Set.range ⇑f) : Maximal (fun (x : β) => x ∈ t) (f x) ↔ Maximal (fun (x : α) => f x ∈ t) x

@[deprecated OrderEmbedding.maximal_apply_mem_iff (since := "2026-04-07")]

theorem OrderEmbedding.maximal_apply_iff {α : Type u_2} {β : Type u_3} {x : α} [Preorder α] [Preorder β] {f : α ↪o β} {t : Set β} (ht : t ⊆ Set.range ⇑f) : Maximal (fun (x : β) => x ∈ t) (f x) ↔ Maximal (fun (x : α) => f x ∈ t) x

Alias of OrderEmbedding.maximal_apply_mem_iff.

theorem OrderEmbedding.image_setOfPred_minimal {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {s : Set α} {f : α ↪o β} : ⇑f '' {x : α | Minimal (fun (x : α) => x ∈ s) x} = {x : β | Minimal (fun (x : β) => x ∈ ⇑f '' s) x}

@[deprecated OrderEmbedding.image_setOfPred_minimal (since := "2026-07-09")]

theorem OrderEmbedding.image_setOf_minimal {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {s : Set α} {f : α ↪o β} : ⇑f '' {x : α | Minimal (fun (x : α) => x ∈ s) x} = {x : β | Minimal (fun (x : β) => x ∈ ⇑f '' s) x}

Alias of OrderEmbedding.image_setOfPred_minimal.

theorem OrderEmbedding.inter_preimage_setOfPred_minimal_eq_of_subset {α : Type u_2} {β : Type u_3} {x : α} [Preorder α] [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_setOfPred_maximal_eq_of_subset {α : Type u_2} {β : Type u_3} {x : α} [Preorder α] [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

@[deprecated OrderEmbedding.inter_preimage_setOfPred_minimal_eq_of_subset (since := "2026-07-09")]

theorem OrderEmbedding.inter_preimage_setOf_minimal_eq_of_subset {α : Type u_2} {β : Type u_3} {x : α} [Preorder α] [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

Alias of OrderEmbedding.inter_preimage_setOfPred_minimal_eq_of_subset.

@[deprecated OrderEmbedding.inter_preimage_setOfPred_maximal_eq_of_subset (since := "2026-07-09")]

theorem OrderEmbedding.inter_preimage_setOf_maximal_eq_of_subset {α : Type u_2} {β : Type u_3} {x : α} [Preorder α] [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

Alias of OrderEmbedding.inter_preimage_setOfPred_maximal_eq_of_subset.

theorem OrderIso.image_setOfPred_minimal {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ≃o β) (P : α → Prop) : ⇑f '' {x : α | Minimal P x} = {x : β | Minimal (fun (x : β) => P (f.symm x)) x}

theorem OrderIso.image_setOfPred_maximal {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ≃o β) (P : α → Prop) : ⇑f '' {x : α | Maximal P x} = {x : β | Maximal (fun (x : β) => P (f.symm x)) x}

@[deprecated OrderIso.image_setOfPred_minimal (since := "2026-07-09")]

theorem OrderIso.image_setOf_minimal {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ≃o β) (P : α → Prop) : ⇑f '' {x : α | Minimal P x} = {x : β | Minimal (fun (x : β) => P (f.symm x)) x}

Alias of OrderIso.image_setOfPred_minimal.

@[deprecated OrderIso.image_setOfPred_maximal (since := "2026-07-09")]

theorem OrderIso.image_setOf_maximal {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α ≃o β) (P : α → Prop) : ⇑f '' {x : α | Maximal P x} = {x : β | Maximal (fun (x : β) => P (f.symm x)) x}

Alias of OrderIso.image_setOfPred_maximal.

theorem OrderIso.map_minimal_mem {α : Type u_2} {β : Type u_3} {x : α} [Preorder α] [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} {β : Type u_3} {x : α} [Preorder α] [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.mapSetOfPredMinimal {α : Type u_2} {β : Type u_3} [Preorder α] [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.

@[deprecated OrderIso.mapSetOfPredMinimal (since := "2026-07-28")]

def OrderIso.mapSetOfMinimal {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {s : Set α} {t : Set β} (f : ↑s ≃o ↑t) : ↑{x : α | Minimal (fun (x : α) => x ∈ s) x} ≃o ↑{x : β | Minimal (fun (x : β) => x ∈ t) x}

Alias of OrderIso.mapSetOfPredMinimal.

---

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

Equations

• @OrderIso.mapSetOfMinimal = @OrderIso.mapSetOfPredMinimal

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

@[deprecated OrderIso.mapSetOfPredMaximal (since := "2026-07-28")]

def OrderIso.mapSetOfMaximal {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {s : Set α} {t : Set β} (f : ↑s ≃o ↑t) : ↑{x : α | Maximal (fun (x : α) => x ∈ s) x} ≃o ↑{x : β | Maximal (fun (x : β) => x ∈ t) x}

Alias of OrderIso.mapSetOfPredMaximal.

---

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

Equations

• @OrderIso.mapSetOfMaximal = @OrderIso.mapSetOfPredMaximal

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

@[deprecated OrderIso.setOfPredMinimalIsoSetOfPredMaximal (since := "2026-07-09")]

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

Alias of OrderIso.setOfPredMinimalIsoSetOfPredMaximal.

---

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

Equations

• @OrderIso.setOfMinimalIsoSetOfMaximal = @OrderIso.setOfPredMinimalIsoSetOfPredMaximal

@[deprecated OrderIso.setOfPredMaximalIsoSetOfPredMinimal (since := "2026-07-09")]

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

Alias of OrderIso.setOfPredMaximalIsoSetOfPredMinimal.

---

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

Equations

• @OrderIso.setOfMaximalIsoSetOfMinimal = @OrderIso.setOfPredMaximalIsoSetOfPredMinimal

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 : b ≤ a) : Maximal (fun (x : α) => x ∈ Set.Icc b a) x ↔ x = a

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 : b < a) : Maximal (fun (x : α) => x ∈ Set.Ioc b a) x ↔ x = a