doc-next-gen

Mathlib.Order.Minimal

Module docstring

{"# 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 "}
minimal_toDual theorem
: Minimal (fun x ↦ P (ofDual x)) (toDual x) ↔ Maximal P x
Full source 
@[simp] theorem minimal_toDual : MinimalMinimal (fun x ↦ P (ofDual x)) (toDual x) ↔ Maximal P x :=
  Iff.rfl
Duality Between Minimality and Maximality via Order Reversal
Informal description
Let $P$ be a predicate on a preorder $\alpha$, and let $x \in \alpha$. Then $x$ is maximal with respect to $P$ if and only if its dual element (under the order-reversing equivalence) is minimal with respect to the predicate $P \circ \text{ofDual}$. More precisely, for the order-reversing equivalence $\text{toDual} : \alpha \to \alpha^\text{dual}$ and its inverse $\text{ofDual} : \alpha^\text{dual} \to \alpha$, we have: $$\text{Minimal} (P \circ \text{ofDual}) (\text{toDual}\, x) \leftrightarrow \text{Maximal}\, P\, x$$
maximal_toDual theorem
: Maximal (fun x ↦ P (ofDual x)) (toDual x) ↔ Minimal P x
Full source 
@[simp] theorem maximal_toDual : MaximalMaximal (fun x ↦ P (ofDual x)) (toDual x) ↔ Minimal P x :=
  Iff.rfl
Duality Between Maximality and Minimality via Order Reversal
Informal description
Let $P$ be a predicate on a preorder $\alpha$, and let $x \in \alpha$. Then $x$ is minimal with respect to $P$ if and only if its dual element (under the order-reversing equivalence) is maximal with respect to the predicate $P \circ \text{ofDual}$. More precisely, for the order-reversing equivalence $\text{toDual} : \alpha \to \alpha^\text{dual}$ and its inverse $\text{ofDual} : \alpha^\text{dual} \to \alpha$, we have: $$\text{Maximal} (P \circ \text{ofDual}) (\text{toDual}\, x) \leftrightarrow \text{Minimal}\, P\, x$$
minimal_false theorem
: ¬Minimal (fun _ ↦ False) x
Full source 
@[simp] theorem minimal_false : ¬ Minimal (fun _ ↦ False) x := by
  simp [Minimal]
No element is minimal with respect to the false predicate
Informal description
For any element $x$ in a preorder, $x$ is not minimal with respect to the always-false predicate.
maximal_false theorem
: ¬Maximal (fun _ ↦ False) x
Full source 
@[simp] theorem maximal_false : ¬ Maximal (fun _ ↦ False) x := by
  simp [Maximal]
No element is maximal with respect to the false predicate
Informal description
For any element $x$ in a preorder, $x$ is not maximal with respect to the always-false predicate.
minimal_true theorem
: Minimal (fun _ ↦ True) x ↔ IsMin x
Full source 
@[simp] theorem minimal_true : MinimalMinimal (fun _ ↦ True) x ↔ IsMin x := by
  simp [IsMin, Minimal]
Minimality with respect to true predicate is equivalent to being minimal in the preorder
Informal description
An element $x$ of a preorder is minimal with respect to the always-true predicate if and only if $x$ is a minimal element in the preorder (i.e., no element is strictly less than $x$).
maximal_true theorem
: Maximal (fun _ ↦ True) x ↔ IsMax x
Full source 
@[simp] theorem maximal_true : MaximalMaximal (fun _ ↦ True) x ↔ IsMax x :=
  minimal_true (α := αᵒᵈ)
Maximality with respect to true predicate is equivalent to being maximal in the preorder
Informal description
An element $x$ of a preorder is maximal with respect to the always-true predicate if and only if $x$ is a maximal element in the preorder (i.e., no element is strictly greater than $x$).
minimal_subtype theorem
{x : Subtype Q} : Minimal (fun x ↦ P x.1) x ↔ Minimal (P ⊓ Q) x
Full source 
@[simp] theorem minimal_subtype {x : Subtype Q} :
    MinimalMinimal (fun x ↦ P x.1) x ↔ Minimal (P ⊓ Q) x := by
  obtain ⟨x, hx⟩ := x
  simp only [Minimal, Subtype.forall, Subtype.mk_le_mk, Pi.inf_apply, inf_Prop_eq]
  tauto
Minimality in Subtype vs. Minimality under Conjunction
Informal description
For an element $x$ in the subtype defined by a predicate $Q$, $x$ is minimal with respect to the predicate $P$ restricted to the subtype if and only if $x$ is minimal with respect to the conjunction $P \cap Q$ in the original type.
maximal_subtype theorem
{x : Subtype Q} : Maximal (fun x ↦ P x.1) x ↔ Maximal (P ⊓ Q) x
Full source 
@[simp] theorem maximal_subtype {x : Subtype Q} :
    MaximalMaximal (fun x ↦ P x.1) x ↔ Maximal (P ⊓ Q) x :=
  minimal_subtype (α := αᵒᵈ)
Maximality in Subtype vs. Maximality under Conjunction
Informal description
For an element $x$ in the subtype defined by a predicate $Q$, $x$ is maximal with respect to the predicate $P$ restricted to the subtype if and only if $x$ is maximal with respect to the conjunction $P \cap Q$ in the original type.
maximal_true_subtype theorem
{x : Subtype P} : Maximal (fun _ ↦ True) x ↔ Maximal P x
Full source 
theorem maximal_true_subtype {x : Subtype P} : MaximalMaximal (fun _ ↦ True) x ↔ Maximal P x := by
  obtain ⟨x, hx⟩ := x
  simp [Maximal, hx]
Maximality in Subtype with Trivial Predicate
Informal description
For any element $x$ in the subtype defined by a predicate $P$, $x$ is maximal with respect to the always-true predicate if and only if $x$ is maximal with respect to $P$.
minimal_true_subtype theorem
{x : Subtype P} : Minimal (fun _ ↦ True) x ↔ Minimal P x
Full source 
theorem minimal_true_subtype {x : Subtype P} : MinimalMinimal (fun _ ↦ True) x ↔ Minimal P x := by
  obtain ⟨x, hx⟩ := x
  simp [Minimal, hx]
Minimality with Respect to True Predicate in Subtype
Informal description
For any element $x$ in the subtype defined by a predicate $P$, the statement that $x$ is minimal with respect to the always-true predicate is equivalent to $x$ being minimal with respect to $P$.
minimal_iff_isMin theorem
(hP : ∀ ⦃x y⦄, P y → x ≤ y → P x) : Minimal P x ↔ P x ∧ IsMin x
Full source 
/-- If `P` is down-closed, then minimal elements satisfying `P` are exactly the globally minimal
elements satisfying `P`. -/
theorem minimal_iff_isMin (hP : ∀ ⦃x y⦄, P y → x ≤ y → P x) : MinimalMinimal P x ↔ P x ∧ IsMin x :=
  ⟨fun h ↦ ⟨h.prop, fun _ h' ↦ h.le_of_le (hP h.prop h') h'⟩, fun h ↦ ⟨h.1, fun _ _  h' ↦ h.2 h'⟩⟩
Characterization of Minimal Elements for Down-Closed Predicates
Informal description
Let $P$ be a predicate on a preordered type $\alpha$ that is down-closed (i.e., for any $x, y \in \alpha$, if $P(y)$ holds and $x \leq y$, then $P(x)$ holds). Then an element $x \in \alpha$ is minimal with respect to $P$ if and only if $x$ satisfies $P$ and is a minimal element in $\alpha$ (i.e., no element is strictly less than $x$).
maximal_iff_isMax theorem
(hP : ∀ ⦃x y⦄, P y → y ≤ x → P x) : Maximal P x ↔ P x ∧ IsMax x
Full source 
/-- If `P` is up-closed, then maximal elements satisfying `P` are exactly the globally maximal
elements satisfying `P`. -/
theorem maximal_iff_isMax (hP : ∀ ⦃x y⦄, P y → y ≤ x → P x) : MaximalMaximal P x ↔ P x ∧ IsMax x :=
  ⟨fun h ↦ ⟨h.prop, fun _ h' ↦ h.le_of_ge (hP h.prop h') h'⟩, fun h ↦ ⟨h.1, fun _ _  h' ↦ h.2 h'⟩⟩
Characterization of Maximal Elements for Up-Closed Predicates
Informal description
Let $P$ be an up-closed predicate on a preordered type $\alpha$ (i.e., for any $x, y \in \alpha$, if $P(y)$ holds and $y \leq x$, then $P(x)$ holds). Then an element $x \in \alpha$ is maximal with respect to $P$ if and only if $x$ satisfies $P$ and is a maximal element in $\alpha$ (i.e., for any $y \in \alpha$, if $x \leq y$ then $y \leq x$). In symbols: $$ \text{Maximal}(P, x) \leftrightarrow P(x) \land \text{IsMax}(x) $$
Minimal.mono theorem
(h : Minimal P x) (hle : Q ≤ P) (hQ : Q x) : Minimal Q x
Full source 
theorem Minimal.mono (h : Minimal P x) (hle : Q ≤ P) (hQ : Q x) : Minimal Q x :=
  ⟨hQ, fun y hQy ↦ h.le_of_le (hle y hQy)⟩
Minimality is Preserved Under Weakening of Predicate
Informal description
Let $P$ and $Q$ be predicates on an ordered type $\alpha$. If $x$ is minimal with respect to $P$, and $Q$ implies $P$ (i.e., $Q \leq P$), and $Q(x)$ holds, then $x$ is also minimal with respect to $Q$.
Maximal.mono theorem
(h : Maximal P x) (hle : Q ≤ P) (hQ : Q x) : Maximal Q x
Full source 
theorem Maximal.mono (h : Maximal P x) (hle : Q ≤ P) (hQ : Q x) : Maximal Q x :=
  ⟨hQ, fun y hQy ↦ h.le_of_ge (hle y hQy)⟩
Monotonicity of Maximality under Predicate Implication
Informal description
Let $P$ and $Q$ be predicates on an ordered type $\alpha$, and let $x \in \alpha$. If $x$ is maximal with respect to $P$, $Q$ implies $P$ (i.e., $Q \leq P$), and $Q(x)$ holds, then $x$ is also maximal with respect to $Q$.
Minimal.and_right theorem
(h : Minimal P x) (hQ : Q x) : Minimal (fun x ↦ P x ∧ Q x) x
Full source 
theorem Minimal.and_right (h : Minimal P x) (hQ : Q x) : Minimal (fun x ↦ P x ∧ Q x) x :=
  h.mono (fun _ ↦ And.left) ⟨h.prop, hQ⟩
Minimality is Preserved Under Conjunction with Additional Predicate
Informal description
Let $P$ and $Q$ be predicates on an ordered type $\alpha$, and let $x \in \alpha$. If $x$ is minimal with respect to $P$ and $Q(x)$ holds, then $x$ is also minimal with respect to the conjunction $P(x) \land Q(x)$.
Minimal.and_left theorem
(h : Minimal P x) (hQ : Q x) : Minimal (fun x ↦ (Q x ∧ P x)) x
Full source 
theorem Minimal.and_left (h : Minimal P x) (hQ : Q x) : Minimal (fun x ↦ (Q x ∧ P x)) x :=
  h.mono (fun _ ↦ And.right) ⟨hQ, h.prop⟩
Minimality is Preserved Under Left Conjunction with Additional Predicate
Informal description
Let $P$ and $Q$ be predicates on an ordered type $\alpha$, and let $x \in \alpha$. If $x$ is minimal with respect to $P$ and $Q(x)$ holds, then $x$ is also minimal with respect to the conjunction $Q(x) \land P(x)$.
Maximal.and_right theorem
(h : Maximal P x) (hQ : Q x) : Maximal (fun x ↦ (P x ∧ Q x)) x
Full source 
theorem Maximal.and_right (h : Maximal P x) (hQ : Q x) : Maximal (fun x ↦ (P x ∧ Q x)) x :=
  h.mono (fun _ ↦ And.left) ⟨h.prop, hQ⟩
Maximality is Preserved Under Conjunction with Additional Predicate
Informal description
Let $P$ and $Q$ be predicates on an ordered type $\alpha$, and let $x \in \alpha$. If $x$ is maximal with respect to $P$ and $Q(x)$ holds, then $x$ is also maximal with respect to the conjunction $P(x) \land Q(x)$.
Maximal.and_left theorem
(h : Maximal P x) (hQ : Q x) : Maximal (fun x ↦ (Q x ∧ P x)) x
Full source 
theorem Maximal.and_left (h : Maximal P x) (hQ : Q x) : Maximal (fun x ↦ (Q x ∧ P x)) x :=
  h.mono (fun _ ↦ And.right) ⟨hQ, h.prop⟩
Maximality Preservation under Left Conjunction with Additional Predicate
Informal description
Let $P$ and $Q$ be predicates on an ordered type $\alpha$, and let $x \in \alpha$. If $x$ is maximal with respect to $P$ and $Q(x)$ holds, then $x$ is also maximal with respect to the conjunction $Q \land P$.
minimal_eq_iff theorem
: Minimal (· = y) x ↔ x = y
Full source 
@[simp] theorem minimal_eq_iff : MinimalMinimal (· = y) x ↔ x = y := by
  simp +contextual [Minimal]
Minimality of Equality Predicate: $x$ is minimal for $\cdot = y$ iff $x = y$
Informal description
An element $x$ is minimal with respect to the predicate $\lambda z, z = y$ if and only if $x = y$.
maximal_eq_iff theorem
: Maximal (· = y) x ↔ x = y
Full source 
@[simp] theorem maximal_eq_iff : MaximalMaximal (· = y) x ↔ x = y := by
  simp +contextual [Maximal]
Maximality of Equality Predicate: $x$ is maximal for $\cdot = y$ iff $x = y$
Informal description
An element $x$ is maximal with respect to the predicate $\lambda z, z = y$ if and only if $x = y$.
not_minimal_iff theorem
(hx : P x) : ¬Minimal P x ↔ ∃ y, P y ∧ y ≤ x ∧ ¬(x ≤ y)
Full source 
theorem not_minimal_iff (hx : P x) : ¬ Minimal P x¬ Minimal P x ↔ ∃ y, P y ∧ y ≤ x ∧ ¬ (x ≤ y) := by
  simp [Minimal, hx]
Characterization of Non-Minimal Elements: $\neg \text{Minimal}(P, x) \leftrightarrow \exists y, P(y) \land y \leq x \land \neg(x \leq y)$
Informal description
For an element $x$ satisfying a predicate $P$ in an ordered type, $x$ is not minimal with respect to $P$ if and only if there exists an element $y$ such that $P(y)$ holds, $y \leq x$, and $x \not\leq y$.
not_maximal_iff theorem
(hx : P x) : ¬Maximal P x ↔ ∃ y, P y ∧ x ≤ y ∧ ¬(y ≤ x)
Full source 
theorem not_maximal_iff (hx : P x) : ¬ Maximal P x¬ Maximal P x ↔ ∃ y, P y ∧ x ≤ y ∧ ¬ (y ≤ x) :=
  not_minimal_iff (α := αᵒᵈ) hx
Characterization of Non-Maximal Elements: $\neg \text{Maximal}(P, x) \leftrightarrow \exists y, P(y) \land x \leq y \land \neg(y \leq x)$
Informal description
For an element $x$ satisfying a predicate $P$ in an ordered type, $x$ is not maximal with respect to $P$ if and only if there exists an element $y$ such that $P(y)$ holds, $x \leq y$, and $y \not\leq x$.
Minimal.or theorem
(h : Minimal (fun x ↦ P x ∨ Q x) x) : Minimal P x ∨ Minimal Q x
Full source 
theorem Minimal.or (h : Minimal (fun x ↦ P x ∨ Q x) x) : MinimalMinimal P x ∨ Minimal Q x := by
  obtain ⟨h | h, hmin⟩ := h
  · exact .inl ⟨h, fun y hy hyx ↦ hmin (Or.inl hy) hyx⟩
  exact .inr ⟨h, fun y hy hyx ↦ hmin (Or.inr hy) hyx⟩
Minimality under Disjunction Implies Minimality under One Predicate
Informal description
Let $P$ and $Q$ be predicates on an ordered type $\alpha$. If an element $x$ is minimal with respect to the predicate $P \lor Q$ (i.e., $x$ is minimal among all elements satisfying $P$ or $Q$), then $x$ is either minimal with respect to $P$ or minimal with respect to $Q$.
Maximal.or theorem
(h : Maximal (fun x ↦ P x ∨ Q x) x) : Maximal P x ∨ Maximal Q x
Full source 
theorem Maximal.or (h : Maximal (fun x ↦ P x ∨ Q x) x) : MaximalMaximal P x ∨ Maximal Q x :=
  Minimal.or (α := αᵒᵈ) h
Maximality under Disjunction Implies Maximality under One Predicate
Informal description
Let $P$ and $Q$ be predicates on an ordered type $\alpha$. If an element $x$ is maximal with respect to the predicate $P \lor Q$ (i.e., $x$ is maximal among all elements satisfying $P$ or $Q$), then $x$ is either maximal with respect to $P$ or maximal with respect to $Q$.
minimal_and_iff_right_of_imp theorem
(hPQ : ∀ ⦃x⦄, P x → Q x) : Minimal (fun x ↦ P x ∧ Q x) x ↔ (Minimal P x) ∧ Q x
Full source 
theorem minimal_and_iff_right_of_imp (hPQ : ∀ ⦃x⦄, P x → Q x) :
    MinimalMinimal (fun x ↦ P x ∧ Q x) x ↔ (Minimal P x) ∧ Q x := by
  simp_rw [and_iff_left_of_imp (fun x ↦ hPQ x), iff_self_and]
  exact fun h ↦ hPQ h.prop
Minimality of Conjunction under Implication Condition
Informal description
Let $P$ and $Q$ be predicates on an ordered type $\alpha$ such that $P(x)$ implies $Q(x)$ for all $x \in \alpha$. Then an element $x \in \alpha$ is minimal with respect to the predicate $P \land Q$ (i.e., $P(x) \land Q(x)$ holds and no smaller element satisfies $P \land Q$) if and only if $x$ is minimal with respect to $P$ and $Q(x)$ holds.
minimal_and_iff_left_of_imp theorem
(hPQ : ∀ ⦃x⦄, P x → Q x) : Minimal (fun x ↦ Q x ∧ P x) x ↔ Q x ∧ (Minimal P x)
Full source 
theorem minimal_and_iff_left_of_imp (hPQ : ∀ ⦃x⦄, P x → Q x) :
    MinimalMinimal (fun x ↦ Q x ∧ P x) x ↔ Q x ∧ (Minimal P x) := by
  simp_rw [iff_comm, and_comm, minimal_and_iff_right_of_imp hPQ, and_comm]
Minimality of Conjunction (Reversed) under Implication Condition
Informal description
Let $P$ and $Q$ be predicates on an ordered type $\alpha$ such that $P(x)$ implies $Q(x)$ for all $x \in \alpha$. Then an element $x \in \alpha$ is minimal with respect to the predicate $Q \land P$ (i.e., $Q(x) \land P(x)$ holds and no smaller element satisfies $Q \land P$) if and only if $Q(x)$ holds and $x$ is minimal with respect to $P$.
maximal_and_iff_right_of_imp theorem
(hPQ : ∀ ⦃x⦄, P x → Q x) : Maximal (fun x ↦ P x ∧ Q x) x ↔ (Maximal P x) ∧ Q x
Full source 
theorem maximal_and_iff_right_of_imp (hPQ : ∀ ⦃x⦄, P x → Q x) :
    MaximalMaximal (fun x ↦ P x ∧ Q x) x ↔ (Maximal P x) ∧ Q x :=
  minimal_and_iff_right_of_imp (α := αᵒᵈ) hPQ
Maximality of Conjunction under Implication Condition
Informal description
Let $P$ and $Q$ be predicates on an ordered type $\alpha$ such that $P(x)$ implies $Q(x)$ for all $x \in \alpha$. Then an element $x \in \alpha$ is maximal with respect to the predicate $P \land Q$ (i.e., $P(x) \land Q(x)$ holds and no larger element satisfies $P \land Q$) if and only if $x$ is maximal with respect to $P$ and $Q(x)$ holds.
maximal_and_iff_left_of_imp theorem
(hPQ : ∀ ⦃x⦄, P x → Q x) : Maximal (fun x ↦ Q x ∧ P x) x ↔ Q x ∧ (Maximal P x)
Full source 
theorem maximal_and_iff_left_of_imp (hPQ : ∀ ⦃x⦄, P x → Q x) :
    MaximalMaximal (fun x ↦ Q x ∧ P x) x ↔ Q x ∧ (Maximal P x) :=
  minimal_and_iff_left_of_imp (α := αᵒᵈ) hPQ
Maximality of Conjunction (Reversed) under Implication Condition
Informal description
Let $P$ and $Q$ be predicates on an ordered type $\alpha$ such that $P(x)$ implies $Q(x)$ for all $x \in \alpha$. Then an element $x \in \alpha$ is maximal with respect to the predicate $Q \land P$ (i.e., $Q(x) \land P(x)$ holds and no larger element satisfies $Q \land P$) if and only if $Q(x)$ holds and $x$ is maximal with respect to $P$.
Minimal.not_prop_of_lt theorem
(h : Minimal P x) (hlt : y < x) : ¬P y
Full source 
theorem Minimal.not_prop_of_lt (h : Minimal P x) (hlt : y < x) : ¬ P y :=
  (minimal_iff_forall_lt.1 h).2 hlt
Minimal Elements Have No Smaller Satisfying Elements
Informal description
If $x$ is a minimal element with respect to a predicate $P$ and $y < x$, then $P(y)$ does not hold.
Maximal.not_prop_of_gt theorem
(h : Maximal P x) (hlt : x < y) : ¬P y
Full source 
theorem Maximal.not_prop_of_gt (h : Maximal P x) (hlt : x < y) : ¬ P y :=
  (maximal_iff_forall_gt.1 h).2 hlt
Maximal Elements Have No Larger Satisfying Elements
Informal description
If $x$ is a maximal element with respect to a predicate $P$ and $x < y$, then $P(y)$ does not hold.
Minimal.not_lt theorem
(h : Minimal P x) (hy : P y) : ¬(y < x)
Full source 
theorem Minimal.not_lt (h : Minimal P x) (hy : P y) : ¬ (y < x) :=
  fun hlt ↦ h.not_prop_of_lt hlt hy
No Smaller Satisfying Elements for Minimal Elements
Informal description
If $x$ is a minimal element with respect to a predicate $P$ and $y$ satisfies $P$, then $y$ is not less than $x$.
Maximal.not_gt theorem
(h : Maximal P x) (hy : P y) : ¬(x < y)
Full source 
theorem Maximal.not_gt (h : Maximal P x) (hy : P y) : ¬ (x < y) :=
  fun hlt ↦ h.not_prop_of_gt hlt hy
Maximal Elements Are Not Strictly Less Than Any Satisfying Element
Informal description
If $x$ is a maximal element with respect to a predicate $P$ and $y$ satisfies $P$, then $x$ is not strictly less than $y$.
minimal_le_iff theorem
: Minimal (· ≤ y) x ↔ x ≤ y ∧ IsMin x
Full source 
@[simp] theorem minimal_le_iff : MinimalMinimal (· ≤ y) x ↔ x ≤ y ∧ IsMin x :=
  minimal_iff_isMin (fun _ _ h h' ↦ h'.trans h)
Characterization of Minimal Elements for Non-Strict Less-Than Predicate: $\text{Minimal}(\cdot \leq y, x) \leftrightarrow x \leq y \land \text{IsMin}(x)$
Informal description
An element $x$ in a preordered type $\alpha$ is minimal with respect to the predicate $\cdot \leq y$ if and only if $x \leq y$ and $x$ is a minimal element in $\alpha$ (i.e., no element is strictly less than $x$).
maximal_ge_iff theorem
: Maximal (y ≤ ·) x ↔ y ≤ x ∧ IsMax x
Full source 
@[simp] theorem maximal_ge_iff : MaximalMaximal (y ≤ ·) x ↔ y ≤ x ∧ IsMax x :=
  minimal_le_iff (α := αᵒᵈ)
Characterization of Maximal Elements for Non-Strict Greater-Than Predicate: $\text{Maximal}(y \leq \cdot, x) \leftrightarrow y \leq x \land \text{IsMax}(x)$
Informal description
An element $x$ in a preordered type $\alpha$ is maximal with respect to the predicate $y \leq \cdot$ if and only if $y \leq x$ and $x$ is a maximal element in $\alpha$ (i.e., no element is strictly greater than $x$).
minimal_lt_iff theorem
: Minimal (· < y) x ↔ x < y ∧ IsMin x
Full source 
@[simp] theorem minimal_lt_iff : MinimalMinimal (· < y) x ↔ x < y ∧ IsMin x :=
  minimal_iff_isMin (fun _ _ h h' ↦ h'.trans_lt h)
Characterization of Minimal Elements for Strictly Less-Than Predicate: $\text{Minimal}(\cdot < y, x) \leftrightarrow x < y \land \text{IsMin}(x)$
Informal description
An element $x$ in an ordered type $\alpha$ is minimal with respect to the predicate $\cdot < y$ if and only if $x < y$ and $x$ is a minimal element in $\alpha$ (i.e., no element is strictly less than $x$).
maximal_gt_iff theorem
: Maximal (y < ·) x ↔ y < x ∧ IsMax x
Full source 
@[simp] theorem maximal_gt_iff : MaximalMaximal (y < ·) x ↔ y < x ∧ IsMax x :=
  minimal_lt_iff (α := αᵒᵈ)
Characterization of Maximal Elements for Strictly Greater-Than Predicate: $\text{Maximal}(y < \cdot, x) \leftrightarrow y < x \land \text{IsMax}(x)$
Informal description
An element $x$ in a preordered type $\alpha$ is maximal with respect to the predicate $y < \cdot$ if and only if $y < x$ and $x$ is a maximal element in $\alpha$ (i.e., no element is strictly greater than $x$).
not_minimal_iff_exists_lt theorem
(hx : P x) : ¬Minimal P x ↔ ∃ y, y < x ∧ P y
Full source 
theorem not_minimal_iff_exists_lt (hx : P x) : ¬ Minimal P x¬ Minimal P x ↔ ∃ y, y < x ∧ P y := by
  simp_rw [not_minimal_iff hx, lt_iff_le_not_le, and_comm]
Existence of Smaller Element Characterizes Non-Minimality: $\neg \text{Minimal}(P, x) \leftrightarrow \exists y, y < x \land P(y)$
Informal description
For an element $x$ satisfying a predicate $P$ in an ordered type, $x$ is not minimal with respect to $P$ if and only if there exists an element $y$ such that $y < x$ and $P(y)$ holds.
not_maximal_iff_exists_gt theorem
(hx : P x) : ¬Maximal P x ↔ ∃ y, x < y ∧ P y
Full source 
theorem not_maximal_iff_exists_gt (hx : P x) : ¬ Maximal P x¬ Maximal P x ↔ ∃ y, x < y ∧ P y :=
  not_minimal_iff_exists_lt (α := αᵒᵈ) hx
Existence of Larger Element Characterizes Non-Maximality: $\neg \text{Maximal}(P, x) \leftrightarrow \exists y, x < y \land P(y)$
Informal description
For an element $x$ satisfying a predicate $P$ in an ordered type, $x$ is not maximal with respect to $P$ if and only if there exists an element $y$ such that $x < y$ and $P(y)$ holds.
minimal_iff theorem
: Minimal P x ↔ P x ∧ ∀ ⦃y⦄, P y → y ≤ x → x = y
Full source 
theorem minimal_iff : MinimalMinimal P x ↔ P x ∧ ∀ ⦃y⦄, P y → y ≤ x → x = y :=
  ⟨fun h ↦ ⟨h.1, fun _ ↦ h.eq_of_ge⟩, fun h ↦ ⟨h.1, fun _ hy hle ↦ (h.2 hy hle).le⟩⟩
Characterization of Minimal Elements with Respect to a Predicate
Informal description
An element $x$ of an ordered type $\alpha$ is minimal with respect to a predicate $P$ if and only if $P(x)$ holds and for any element $y$ satisfying $P(y)$, if $y \leq x$ then $x = y$.
minimal_iff_eq theorem
(hy : P y) (hP : ∀ ⦃x⦄, P x → y ≤ x) : Minimal P x ↔ x = y
Full source 
/-- If `P y` holds, and everything satisfying `P` is above `y`, then `y` is the unique minimal
element satisfying `P`. -/
theorem minimal_iff_eq (hy : P y) (hP : ∀ ⦃x⦄, P x → y ≤ x) : MinimalMinimal P x ↔ x = y :=
  ⟨fun h ↦ h.eq_of_ge hy (hP h.prop), by rintro rfl; exact ⟨hy, fun z hz _ ↦ hP hz⟩⟩
Characterization of Minimal Elements: Minimality is Equivalent to Equality with Lower Bound
Informal description
Let $P$ be a predicate on an ordered type $\alpha$, and let $y$ be an element such that $P(y)$ holds. If every element $x$ satisfying $P(x)$ is greater than or equal to $y$, then for any element $x$, the statement that $x$ is minimal with respect to $P$ is equivalent to $x = y$.
maximal_iff_eq theorem
(hy : P y) (hP : ∀ ⦃x⦄, P x → x ≤ y) : Maximal P x ↔ x = y
Full source 
/-- If `P y` holds, and everything satisfying `P` is below `y`, then `y` is the unique maximal
element satisfying `P`. -/
theorem maximal_iff_eq (hy : P y) (hP : ∀ ⦃x⦄, P x → x ≤ y) : MaximalMaximal P x ↔ x = y :=
  minimal_iff_eq (α := αᵒᵈ) hy hP
Characterization of Maximal Elements: Maximality is Equivalent to Equality with Upper Bound
Informal description
Let $P$ be a predicate on an ordered type $\alpha$, and let $y$ be an element such that $P(y)$ holds. If every element $x$ satisfying $P(x)$ is less than or equal to $y$, then for any element $x$, the statement that $x$ is maximal with respect to $P$ is equivalent to $x = y$.
minimal_ge_iff theorem
: Minimal (y ≤ ·) x ↔ x = y
Full source 
@[simp] theorem minimal_ge_iff : MinimalMinimal (y ≤ ·) x ↔ x = y :=
  minimal_iff_eq rfl.le fun _ ↦ id
Minimality Criterion for Lower Bound: $\text{Minimal}(y \leq \cdot)(x) \leftrightarrow x = y$
Informal description
For any element $x$ in an ordered type $\alpha$, the statement that $x$ is minimal with respect to the predicate $\lambda z, y \leq z$ is equivalent to $x = y$.
maximal_le_iff theorem
: Maximal (· ≤ y) x ↔ x = y
Full source 
@[simp] theorem maximal_le_iff : MaximalMaximal (· ≤ y) x ↔ x = y :=
  maximal_iff_eq rfl.le fun _ ↦ id
Maximality Criterion for Upper Bound: $\text{Maximal}(\cdot \leq y)(x) \leftrightarrow x = y$
Informal description
For any element $x$ in an ordered type $\alpha$, the statement that $x$ is maximal with respect to the predicate $\lambda z, z \leq y$ is equivalent to $x = y$.
minimal_iff_minimal_of_imp_of_forall theorem
(hPQ : ∀ ⦃x⦄, Q x → P x) (h : ∀ ⦃x⦄, P x → ∃ y, y ≤ x ∧ Q y) : Minimal P x ↔ Minimal Q x
Full source 
theorem minimal_iff_minimal_of_imp_of_forall (hPQ : ∀ ⦃x⦄, Q x → P x)
    (h : ∀ ⦃x⦄, P x → ∃ y, y ≤ x ∧ Q y) : MinimalMinimal P x ↔ Minimal Q x := by
  refine ⟨fun h' ↦ ⟨?_, fun y hy hyx ↦ h'.le_of_le (hPQ hy) hyx⟩,
    fun h' ↦ ⟨hPQ h'.prop, fun y hy hyx ↦ ?_⟩⟩
  · obtain ⟨y, hyx, hy⟩ := h h'.prop
    rwa [((h'.le_of_le (hPQ hy)) hyx).antisymm hyx]
  obtain ⟨z, hzy, hz⟩ := h hy
  exact (h'.le_of_le hz (hzy.trans hyx)).trans hzy
Minimality Criterion under Predicate Implication and Forall Condition
Informal description
Let $P$ and $Q$ be predicates on an ordered type $\alpha$ such that: 1. For all $x$, if $Q(x)$ holds then $P(x)$ holds. 2. For all $x$ where $P(x)$ holds, there exists $y$ such that $y \leq x$ and $Q(y)$ holds. Then, an element $x$ is minimal with respect to $P$ if and only if it is minimal with respect to $Q$.
maximal_iff_maximal_of_imp_of_forall theorem
(hPQ : ∀ ⦃x⦄, Q x → P x) (h : ∀ ⦃x⦄, P x → ∃ y, x ≤ y ∧ Q y) : Maximal P x ↔ Maximal Q x
Full source 
theorem maximal_iff_maximal_of_imp_of_forall (hPQ : ∀ ⦃x⦄, Q x → P x)
    (h : ∀ ⦃x⦄, P x → ∃ y, x ≤ y ∧ Q y) : MaximalMaximal P x ↔ Maximal Q x :=
  minimal_iff_minimal_of_imp_of_forall (α := αᵒᵈ) hPQ h
Maximality Criterion under Predicate Implication and Forall Condition
Informal description
Let $P$ and $Q$ be predicates on an ordered type $\alpha$ such that: 1. For all $x$, if $Q(x)$ holds then $P(x)$ holds. 2. For all $x$ where $P(x)$ holds, there exists $y$ such that $x \leq y$ and $Q(y)$ holds. Then, an element $x$ is maximal with respect to $P$ if and only if it is maximal with respect to $Q$.
maximal_subset_iff' theorem
: Maximal P s ↔ P s ∧ ∀ ⦃t⦄, P t → s ⊆ t → t ⊆ s
Full source 
theorem maximal_subset_iff' : MaximalMaximal P s ↔ P s ∧ ∀ ⦃t⦄, P t → s ⊆ t → t ⊆ s :=
  Iff.rfl
Characterization of Maximal Sets via Subset Inclusion
Informal description
A set $s$ is maximal with respect to a predicate $P$ if and only if $P(s)$ holds and for any set $t$ satisfying $P(t)$, if $s$ is a subset of $t$, then $t$ is also a subset of $s$. In other words, $s$ is maximal if it is the largest set (under inclusion) satisfying $P$.
not_minimal_subset_iff theorem
(hs : P s) : ¬Minimal P s ↔ ∃ t, t ⊂ s ∧ P t
Full source 
theorem not_minimal_subset_iff (hs : P s) : ¬ Minimal P s¬ Minimal P s ↔ ∃ t, t ⊂ s ∧ P t :=
  not_minimal_iff_exists_lt hs
Existence of Strict Subset Characterizes Non-Minimality: $\neg \text{Minimal}(P, s) \leftrightarrow \exists t, t \subset s \land P(t)$
Informal description
For a set $s$ satisfying a predicate $P$, $s$ is not minimal with respect to $P$ if and only if there exists a set $t$ such that $t$ is a strict subset of $s$ and $P(t)$ holds.
not_maximal_subset_iff theorem
(hs : P s) : ¬Maximal P s ↔ ∃ t, s ⊂ t ∧ P t
Full source 
theorem not_maximal_subset_iff (hs : P s) : ¬ Maximal P s¬ Maximal P s ↔ ∃ t, s ⊂ t ∧ P t :=
  not_maximal_iff_exists_gt hs
Existence of Strictly Larger Set Characterizes Non-Maximality: $\neg \text{Maximal}(P, s) \leftrightarrow \exists t, s \subset t \land P(t)$
Informal description
For a set $s$ satisfying a predicate $P$ in a partially ordered collection of sets, $s$ is not maximal with respect to $P$ if and only if there exists a set $t$ such that $s$ is a strict subset of $t$ and $P(t)$ holds.
Minimal.not_prop_of_ssubset theorem
(h : Minimal P s) (ht : t ⊂ s) : ¬P t
Full source 
theorem Minimal.not_prop_of_ssubset (h : Minimal P s) (ht : t ⊂ s) : ¬ P t :=
  (minimal_iff_forall_lt.1 h).2 ht
Minimal Sets Do Not Contain Proper Subsets Satisfying $P$
Informal description
Let $P$ be a predicate on sets over a type $\alpha$, and let $s$ be a set that is minimal with respect to $P$. If $t$ is a proper subset of $s$ (i.e., $t \subset s$), then $t$ does not satisfy $P$.
Minimal.not_ssubset theorem
(h : Minimal P s) (ht : P t) : ¬t ⊂ s
Full source 
theorem Minimal.not_ssubset (h : Minimal P s) (ht : P t) : ¬ t ⊂ s :=
  h.not_lt ht
No Strict Subset of Minimal Set Satisfies Predicate
Informal description
Let $P$ be a predicate on sets over a type $\alpha$, and let $s$ be a set that is minimal with respect to $P$. For any set $t$ that satisfies $P$, it is not the case that $t$ is a strict subset of $s$.
Maximal.mem_of_prop_insert theorem
(h : Maximal P s) (hx : P (insert x s)) : x ∈ s
Full source 
theorem Maximal.mem_of_prop_insert (h : Maximal P s) (hx : P (insert x s)) : x ∈ s :=
  h.eq_of_subset hx (subset_insert _ _) ▸ mem_insert ..
Maximal Set Property under Insertion
Informal description
Let $P$ be a predicate on sets over a type $\alpha$, and let $s$ be a set that is maximal with respect to $P$. If inserting an element $x$ into $s$ results in a set that still satisfies $P$, then $x$ must already be an element of $s$. In other words, if $P(s \cup \{x\})$ holds, then $x \in s$.
Minimal.not_mem_of_prop_diff_singleton theorem
(h : Minimal P s) (hx : P (s \ { x })) : x ∉ s
Full source 
theorem Minimal.not_mem_of_prop_diff_singleton (h : Minimal P s) (hx : P (s \ {x})) : x ∉ s :=
  fun hxs ↦ ((h.eq_of_superset hx diff_subset).subset hxs).2 rfl
Minimal Set Property under Removal of an Element
Informal description
Let $P$ be a predicate on sets over a type $\alpha$, and let $s$ be a set that is minimal with respect to $P$. If removing an element $x$ from $s$ results in a set that still satisfies $P$, then $x$ must not be an element of $s$. In other words, if $P(s \setminus \{x\})$ holds, then $x \notin s$.
Set.minimal_iff_forall_diff_singleton theorem
(hP : ∀ ⦃s t⦄, P t → t ⊆ s → P s) : Minimal P s ↔ P s ∧ ∀ x ∈ s, ¬P (s \ { x })
Full source 
theorem Set.minimal_iff_forall_diff_singleton (hP : ∀ ⦃s t⦄, P t → t ⊆ s → P s) :
    MinimalMinimal P s ↔ P s ∧ ∀ x ∈ s, ¬ P (s \ {x}) :=
  ⟨fun h ↦ ⟨h.1, fun _ hx hP ↦ h.not_mem_of_prop_diff_singleton hP hx⟩,
    fun h ↦ ⟨h.1, fun _ ht hts x hxs ↦ by_contra fun hxt ↦
      h.2 x hxs (hP ht <| subset_diff_singleton hts hxt)⟩⟩
Characterization of Minimal Sets via Set Difference with Singletons
Informal description
Let $P$ be a predicate on sets over a type $\alpha$ that is upward-closed under subset inclusion (i.e., if $P(t)$ holds and $t \subseteq s$, then $P(s)$ holds). A set $s$ is minimal with respect to $P$ if and only if $P(s)$ holds and for every element $x \in s$, the set difference $s \setminus \{x\}$ does not satisfy $P$.
Set.exists_diff_singleton_of_not_minimal theorem
(hP : ∀ ⦃s t⦄, P t → t ⊆ s → P s) (hs : P s) (h : ¬Minimal P s) : ∃ x ∈ s, P (s \ { x })
Full source 
theorem Set.exists_diff_singleton_of_not_minimal (hP : ∀ ⦃s t⦄, P t → t ⊆ s → P s) (hs : P s)
    (h : ¬ Minimal P s) : ∃ x ∈ s, P (s \ {x}) := by
  simpa [Set.minimal_iff_forall_diff_singleton hP, hs] using h
Existence of Removable Element in Non-Minimal Set Satisfying Upward-Closed Predicate
Informal description
Let $P$ be a predicate on sets over a type $\alpha$ that is upward-closed under subset inclusion (i.e., if $P(t)$ holds and $t \subseteq s$, then $P(s)$ holds). If a set $s$ satisfies $P$ but is not minimal with respect to $P$, then there exists an element $x \in s$ such that the set difference $s \setminus \{x\}$ satisfies $P$.
Maximal.not_prop_of_ssuperset theorem
(h : Maximal P s) (ht : s ⊂ t) : ¬P t
Full source 
theorem Maximal.not_prop_of_ssuperset (h : Maximal P s) (ht : s ⊂ t) : ¬ P t :=
  (maximal_iff_forall_gt.1 h).2 ht
Maximal Sets Do Not Extend to Larger Sets Satisfying $P$
Informal description
If a set $s$ is maximal with respect to a predicate $P$ and $s$ is strictly contained in another set $t$, then $t$ does not satisfy $P$.
Maximal.not_ssuperset theorem
(h : Maximal P s) (ht : P t) : ¬s ⊂ t
Full source 
theorem Maximal.not_ssuperset (h : Maximal P s) (ht : P t) : ¬ s ⊂ t :=
  h.not_gt ht
Maximal Elements Are Not Strictly Contained in Any Satisfying Set
Informal description
If $s$ is a maximal element with respect to a predicate $P$ and $t$ satisfies $P$, then $s$ is not a strict subset of $t$.
Set.maximal_iff_forall_insert theorem
(hP : ∀ ⦃s t⦄, P t → s ⊆ t → P s) : Maximal P s ↔ P s ∧ ∀ x ∉ s, ¬P (insert x s)
Full source 
theorem Set.maximal_iff_forall_insert (hP : ∀ ⦃s t⦄, P t → s ⊆ t → P s) :
    MaximalMaximal P s ↔ P s ∧ ∀ x ∉ s, ¬ P (insert x s) := by
  simp only [not_imp_not]
  exact ⟨fun h ↦ ⟨h.1, fun x ↦ h.mem_of_prop_insert⟩,
    fun h ↦ ⟨h.1, fun t ht hst x hxt ↦ h.2 x (hP ht <| insert_subset hxt hst)⟩⟩
Characterization of Maximal Sets via Insertion
Informal description
Let $P$ be a predicate on sets over a type $\alpha$ that is downward-closed (i.e., if $P(t)$ holds and $s \subseteq t$, then $P(s)$ holds). A set $s$ is maximal with respect to $P$ if and only if $P(s)$ holds and for every element $x \notin s$, the set $\{x\} \cup s$ does not satisfy $P$.
Set.exists_insert_of_not_maximal theorem
(hP : ∀ ⦃s t⦄, P t → s ⊆ t → P s) (hs : P s) (h : ¬Maximal P s) : ∃ x ∉ s, P (insert x s)
Full source 
theorem Set.exists_insert_of_not_maximal (hP : ∀ ⦃s t⦄, P t → s ⊆ t → P s) (hs : P s)
    (h : ¬ Maximal P s) : ∃ x ∉ s, P (insert x s) := by
  simpa [Set.maximal_iff_forall_insert hP, hs] using h
Existence of Insertion Preserving Predicate for Non-Maximal Sets
Informal description
Let $P$ be a predicate on sets over a type $\alpha$ that is downward-closed (i.e., if $P(t)$ holds and $s \subseteq t$, then $P(s)$ holds). If a set $s$ satisfies $P$ but is not maximal with respect to $P$, then there exists an element $x \notin s$ such that the set $\{x\} \cup s$ satisfies $P$.
setOf_maximal_subset theorem
(s : Set α) : {x | Maximal (· ∈ s) x} ⊆ s
Full source 
theorem setOf_maximal_subset (s : Set α) : {x | Maximal (· ∈ s) x}{x | Maximal (· ∈ s) x} ⊆ s :=
  sep_subset ..
Maximal Elements are Contained in the Set
Informal description
For any set $s$ of elements of type $\alpha$, the set of all maximal elements of $s$ is a subset of $s$. Here, an element $x$ is *maximal* in $s$ if for all $y \in s$, $x \leq y$ implies $y \leq x$.
Set.Subsingleton.maximal_mem_iff theorem
(h : s.Subsingleton) : Maximal (· ∈ s) x ↔ x ∈ s
Full source 
theorem Set.Subsingleton.maximal_mem_iff (h : s.Subsingleton) : MaximalMaximal (· ∈ s) x ↔ x ∈ s := by
  obtain (rfl | ⟨x, rfl⟩) := h.eq_empty_or_singleton <;> simp
Maximality in a Subsingleton Set
Informal description
For a subsingleton set $s$ (i.e., a set containing at most one element), an element $x$ is maximal in $s$ if and only if $x$ belongs to $s$.
Set.Subsingleton.minimal_mem_iff theorem
(h : s.Subsingleton) : Minimal (· ∈ s) x ↔ x ∈ s
Full source 
theorem Set.Subsingleton.minimal_mem_iff (h : s.Subsingleton) : MinimalMinimal (· ∈ s) x ↔ x ∈ s := by
  obtain (rfl | ⟨x, rfl⟩) := h.eq_empty_or_singleton <;> simp
Minimality in a Subsingleton Set
Informal description
For a subsingleton set $s$ (i.e., a set containing at most one element) in a partially ordered type $\alpha$, an element $x$ is minimal in $s$ if and only if $x$ belongs to $s$.
IsLeast.minimal theorem
(h : IsLeast s x) : Minimal (· ∈ s) x
Full source 
theorem IsLeast.minimal (h : IsLeast s x) : Minimal (· ∈ s) x :=
  ⟨h.1, fun _b hb _ ↦ h.2 hb⟩
Least Element is Minimal
Informal description
If an element $x$ is the least element of a set $s$ in a partially ordered type $\alpha$, then $x$ is minimal in $s$, meaning there does not exist any $y \in s$ such that $y < x$.
IsGreatest.maximal theorem
(h : IsGreatest s x) : Maximal (· ∈ s) x
Full source 
theorem IsGreatest.maximal (h : IsGreatest s x) : Maximal (· ∈ s) x :=
  ⟨h.1, fun _b hb _ ↦ h.2 hb⟩
Greatest Element is Maximal
Informal description
If an element $x$ is the greatest element of a set $s$ in a partially ordered type $\alpha$, then $x$ is maximal in $s$, meaning there does not exist any $y \in s$ such that $x < y$.
IsAntichain.minimal_mem_iff theorem
(hs : IsAntichain (· ≤ ·) s) : Minimal (· ∈ s) x ↔ x ∈ s
Full source 
theorem IsAntichain.minimal_mem_iff (hs : IsAntichain (· ≤ ·) s) : MinimalMinimal (· ∈ s) x ↔ x ∈ s :=
  ⟨fun h ↦ h.prop, fun h ↦ ⟨h, fun _ hys hyx ↦ (hs.eq hys h hyx).symm.le⟩⟩
Minimal Elements in an Antichain are Exactly its Members
Informal description
For an antichain $s$ in a partially ordered set (i.e., a set where no two distinct elements are comparable), an element $x$ is minimal in $s$ if and only if $x$ is a member of $s$.
IsAntichain.maximal_mem_iff theorem
(hs : IsAntichain (· ≤ ·) s) : Maximal (· ∈ s) x ↔ x ∈ s
Full source 
theorem IsAntichain.maximal_mem_iff (hs : IsAntichain (· ≤ ·) s) : MaximalMaximal (· ∈ s) x ↔ x ∈ s :=
  hs.to_dual.minimal_mem_iff
Maximal Elements in an Antichain are Exactly its Members
Informal description
For an antichain $s$ in a partially ordered set (i.e., a set where no two distinct elements are comparable), an element $x$ is maximal in $s$ if and only if $x$ is a member of $s$.
setOf_maximal_antichain theorem
(P : α → Prop) : IsAntichain (· ≤ ·) {x | Maximal P x}
Full source 
theorem setOf_maximal_antichain (P : α → Prop) : IsAntichain (· ≤ ·) {x | Maximal P x} :=
  fun _ hx _ ⟨hy, _⟩ hne hle ↦ hne (hle.antisymm <| hx.2 hy hle)
Maximal Elements Form an Antichain
Informal description
For any predicate $P$ on an ordered type $\alpha$, the set $\{x \mid \text{Maximal } P x\}$ of all maximal elements satisfying $P$ forms an antichain with respect to the order relation $\leq$.
setOf_minimal_antichain theorem
(P : α → Prop) : IsAntichain (· ≤ ·) {x | Minimal P x}
Full source 
theorem setOf_minimal_antichain (P : α → Prop) : IsAntichain (· ≤ ·) {x | Minimal P x} :=
  (setOf_maximal_antichain (α := αᵒᵈ) P).swap
Minimal Elements Form an Antichain
Informal description
For any predicate $P$ on an ordered type $\alpha$, the set $\{x \mid \text{Minimal } P x\}$ of all minimal elements satisfying $P$ forms an antichain with respect to the order relation $\leq$.
IsLeast.minimal_iff theorem
(h : IsLeast s a) : Minimal (· ∈ s) x ↔ x = a
Full source 
theorem IsLeast.minimal_iff (h : IsLeast s a) : MinimalMinimal (· ∈ s) x ↔ x = a :=
  ⟨fun h' ↦ h'.eq_of_ge h.1 (h.2 h'.prop), fun h' ↦ h' ▸ h.minimal⟩
Characterization of Minimal Elements in Terms of Least Element
Informal description
Let $s$ be a set in a partially ordered type $\alpha$, and let $a$ be the least element of $s$. Then an element $x$ is minimal in $s$ (i.e., there is no $y \in s$ such that $y < x$) if and only if $x = a$.
IsGreatest.maximal_iff theorem
(h : IsGreatest s a) : Maximal (· ∈ s) x ↔ x = a
Full source 
theorem IsGreatest.maximal_iff (h : IsGreatest s a) : MaximalMaximal (· ∈ s) x ↔ x = a :=
  ⟨fun h' ↦ h'.eq_of_le h.1 (h.2 h'.prop), fun h' ↦ h' ▸ h.maximal⟩
Characterization of Maximal Elements in Terms of Greatest Element
Informal description
Let $s$ be a set in a partially ordered type $\alpha$, and let $a$ be the greatest element of $s$. Then an element $x$ is maximal in $s$ (i.e., there is no $y \in s$ such that $x < y$) if and only if $x = a$.
minimal_mem_image_monotone theorem
(hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)) (hx : Minimal (· ∈ s) x) : Minimal (· ∈ f '' s) (f x)
Full source 
theorem minimal_mem_image_monotone (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y))
    (hx : Minimal (· ∈ s) x) : Minimal (· ∈ f '' s) (f x) := by
  refine ⟨mem_image_of_mem f hx.prop, ?_⟩
  rintro _ ⟨y, hy, rfl⟩
  rw [hf hx.prop hy, hf hy hx.prop]
  exact hx.le_of_le hy
Minimality Preservation under Monotone Image Mapping
Informal description
Let $s$ be a subset of a partially ordered type $\alpha$, and let $f : \alpha \to \beta$ be a function such that for all $x, y \in s$, $f(x) \leq f(y)$ if and only if $x \leq y$. If $x$ is a minimal element of $s$ (i.e., there is no $y \in s$ such that $y < x$), then $f(x)$ is a minimal element of the image $f(s)$.
maximal_mem_image_monotone theorem
(hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)) (hx : Maximal (· ∈ s) x) : Maximal (· ∈ f '' s) (f x)
Full source 
theorem maximal_mem_image_monotone (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y))
    (hx : Maximal (· ∈ s) x) : Maximal (· ∈ f '' s) (f x) :=
  minimal_mem_image_monotone (α := αᵒᵈ) (β := βᵒᵈ) (s := s) (fun _ _ hx hy ↦ hf hy hx) hx
Maximality Preservation under Monotone Image Mapping
Informal description
Let $s$ be a subset of a partially ordered type $\alpha$, and let $f : \alpha \to \beta$ be a function such that for all $x, y \in s$, $f(x) \leq f(y)$ if and only if $x \leq y$. If $x$ is a maximal element of $s$ (i.e., there is no $y \in s$ such that $x < y$), then $f(x)$ is a maximal element of the image $f(s)$.
minimal_mem_image_monotone_iff theorem
(ha : a ∈ s) (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)) : Minimal (· ∈ f '' s) (f a) ↔ Minimal (· ∈ s) a
Full source 
theorem minimal_mem_image_monotone_iff (ha : a ∈ s)
    (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)) :
    MinimalMinimal (· ∈ f '' s) (f a) ↔ Minimal (· ∈ s) a := by
  refine ⟨fun h ↦ ⟨ha, fun y hys ↦ ?_⟩, minimal_mem_image_monotone hf⟩
  rw [← hf ha hys, ← hf hys ha]
  exact h.le_of_le (mem_image_of_mem f hys)
Minimality in Image under Monotone Function iff Minimality in Domain
Informal description
Let $s$ be a subset of a partially ordered type $\alpha$, $a \in s$, and $f : \alpha \to \beta$ a function such that for all $x, y \in s$, $f(x) \leq f(y)$ if and only if $x \leq y$. Then $f(a)$ is a minimal element of the image $f(s)$ if and only if $a$ is a minimal element of $s$.
maximal_mem_image_monotone_iff theorem
(ha : a ∈ s) (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)) : Maximal (· ∈ f '' s) (f a) ↔ Maximal (· ∈ s) a
Full source 
theorem maximal_mem_image_monotone_iff (ha : a ∈ s)
    (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)) :
    MaximalMaximal (· ∈ f '' s) (f a) ↔ Maximal (· ∈ s) a :=
  minimal_mem_image_monotone_iff (α := αᵒᵈ) (β := βᵒᵈ) (s := s) ha fun _ _ hx hy ↦ hf hy hx
Maximality in Image under Monotone Function iff Maximality in Domain
Informal description
Let $s$ be a subset of a partially ordered type $\alpha$, $a \in s$, and $f : \alpha \to \beta$ a function such that for all $x, y \in s$, $f(x) \leq f(y)$ if and only if $x \leq y$. Then $f(a)$ is a maximal element of the image $f(s)$ if and only if $a$ is a maximal element of $s$.
minimal_mem_image_antitone theorem
(hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ y ≤ x)) (hx : Minimal (· ∈ s) x) : Maximal (· ∈ f '' s) (f x)
Full source 
theorem minimal_mem_image_antitone (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ y ≤ x))
    (hx : Minimal (· ∈ s) x) : Maximal (· ∈ f '' s) (f x) :=
  minimal_mem_image_monotone (β := βᵒᵈ) (fun _ _ h h' ↦ hf h' h) hx
Minimality Transforms to Maximality under Antitone Image Mapping
Informal description
Let $s$ be a subset of a partially ordered type $\alpha$, and let $f : \alpha \to \beta$ be a function such that for all $x, y \in s$, $f(x) \leq f(y)$ if and only if $y \leq x$. If $x$ is a minimal element of $s$ (i.e., there is no $y \in s$ such that $y < x$), then $f(x)$ is a maximal element of the image $f(s)$.
maximal_mem_image_antitone theorem
(hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ y ≤ x)) (hx : Maximal (· ∈ s) x) : Minimal (· ∈ f '' s) (f x)
Full source 
theorem maximal_mem_image_antitone (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ y ≤ x))
    (hx : Maximal (· ∈ s) x) : Minimal (· ∈ f '' s) (f x) :=
  maximal_mem_image_monotone (β := βᵒᵈ) (fun _ _ h h' ↦ hf h' h) hx
Maximality Transforms to Minimality under Antitone Image Mapping
Informal description
Let $s$ be a subset of a partially ordered type $\alpha$, and let $f : \alpha \to \beta$ be a function such that for all $x, y \in s$, $f(x) \leq f(y)$ if and only if $y \leq x$. If $x$ is a maximal element of $s$ (i.e., there is no $y \in s$ such that $x < y$), then $f(x)$ is a minimal element of the image $f(s)$.
minimal_mem_image_antitone_iff theorem
(ha : a ∈ s) (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ y ≤ x)) : Minimal (· ∈ f '' s) (f a) ↔ Maximal (· ∈ s) a
Full source 
theorem minimal_mem_image_antitone_iff (ha : a ∈ s)
    (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ y ≤ x)) :
    MinimalMinimal (· ∈ f '' s) (f a) ↔ Maximal (· ∈ s) a :=
  maximal_mem_image_monotone_iff (β := βᵒᵈ) ha (fun _ _ h h' ↦ hf h' h)
Minimality in Image under Antitone Function iff Maximality in Domain
Informal description
Let $s$ be a subset of a partially ordered type $\alpha$, $a \in s$, and $f : \alpha \to \beta$ a function such that for all $x, y \in s$, $f(x) \leq f(y)$ if and only if $y \leq x$. Then $f(a)$ is a minimal element of the image $f(s)$ if and only if $a$ is a maximal element of $s$.
maximal_mem_image_antitone_iff theorem
(ha : a ∈ s) (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ y ≤ x)) : Maximal (· ∈ f '' s) (f a) ↔ Minimal (· ∈ s) a
Full source 
theorem maximal_mem_image_antitone_iff (ha : a ∈ s)
    (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ y ≤ x)) :
    MaximalMaximal (· ∈ f '' s) (f a) ↔ Minimal (· ∈ s) a :=
  minimal_mem_image_monotone_iff (β := βᵒᵈ) ha (fun _ _ h h' ↦ hf h' h)
Maximality in Image under Antitone Function iff Minimality in Domain
Informal description
Let $s$ be a subset of a partially ordered type $\alpha$, $a \in s$, and $f : \alpha \to \beta$ a function such that for all $x, y \in s$, $f(x) \leq f(y)$ if and only if $y \leq x$. Then $f(a)$ is a maximal element of the image $f(s)$ if and only if $a$ is a minimal element of $s$.
image_monotone_setOf_minimal theorem
(hf : ∀ ⦃x y⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)) : f '' {x | Minimal P x} = {x | Minimal (∃ x₀, P x₀ ∧ f x₀ = ·) x}
Full source 
theorem image_monotone_setOf_minimal (hf : ∀ ⦃x y⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)) :
    f '' {x | Minimal P x} = {x | Minimal (∃ x₀, P x₀ ∧ f x₀ = ·) x} := by
  refine Set.ext fun x ↦ ⟨?_, fun h ↦ ?_⟩
  · rintro ⟨x, (hx : Minimal _ x), rfl⟩
    exact (minimal_mem_image_monotone_iff hx.prop hf).2 hx
  obtain ⟨y, hy, rfl⟩ := (mem_setOf_eq ▸ h).prop
  exact mem_image_of_mem _ <| (minimal_mem_image_monotone_iff (s := setOf P) hy hf).1 h
Image of Minimal Elements under Monotone Function Equals Minimal Elements of Image Predicate
Informal description
Let $P$ be a predicate on a partially ordered type $\alpha$, and let $f : \alpha \to \beta$ be a function such that for all $x, y$ satisfying $P$, $f(x) \leq f(y)$ if and only if $x \leq y$. Then the image under $f$ of the set of minimal elements of $P$ is equal to the set of minimal elements of the predicate "there exists $x_0$ such that $P(x_0)$ and $f(x_0) = x$".
image_monotone_setOf_maximal theorem
(hf : ∀ ⦃x y⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)) : f '' {x | Maximal P x} = {x | Maximal (∃ x₀, P x₀ ∧ f x₀ = ·) x}
Full source 
theorem image_monotone_setOf_maximal (hf : ∀ ⦃x y⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)) :
    f '' {x | Maximal P x} = {x | Maximal (∃ x₀, P x₀ ∧ f x₀ = ·) x} :=
  image_monotone_setOf_minimal (α := αᵒᵈ) (β := βᵒᵈ) (fun _ _ hx hy ↦ hf hy hx)
Image of Maximal Elements under Monotone Function Equals Maximal Elements of Image Predicate
Informal description
Let $P$ be a predicate on a partially ordered type $\alpha$, and let $f : \alpha \to \beta$ be a function such that for all $x, y$ satisfying $P$, $f(x) \leq f(y)$ if and only if $x \leq y$. Then the image under $f$ of the set of maximal elements of $P$ is equal to the set of maximal elements of the predicate "there exists $x_0$ such that $P(x_0)$ and $f(x_0) = x$".
image_antitone_setOf_minimal theorem
(hf : ∀ ⦃x y⦄, P x → P y → (f x ≤ f y ↔ y ≤ x)) : f '' {x | Minimal P x} = {x | Maximal (∃ x₀, P x₀ ∧ f x₀ = ·) x}
Full source 
theorem image_antitone_setOf_minimal (hf : ∀ ⦃x y⦄, P x → P y → (f x ≤ f y ↔ y ≤ x)) :
    f '' {x | Minimal P x} = {x | Maximal (∃ x₀, P x₀ ∧ f x₀ = ·) x} :=
  image_monotone_setOf_minimal (β := βᵒᵈ) (fun _ _ hx hy ↦ hf hy hx)
Image of Minimal Elements under Antitone Function Equals Maximal Elements of Image Predicate
Informal description
Let $P$ be a predicate on a partially ordered type $\alpha$, and let $f : \alpha \to \beta$ be a function such that for all $x, y$ satisfying $P$, $f(x) \leq f(y)$ if and only if $y \leq x$. Then the image under $f$ of the set of minimal elements of $P$ is equal to the set of maximal elements of the predicate "there exists $x_0$ such that $P(x_0)$ and $f(x_0) = x$".
image_antitone_setOf_maximal theorem
(hf : ∀ ⦃x y⦄, P x → P y → (f x ≤ f y ↔ y ≤ x)) : f '' {x | Maximal P x} = {x | Minimal (∃ x₀, P x₀ ∧ f x₀ = ·) x}
Full source 
theorem image_antitone_setOf_maximal (hf : ∀ ⦃x y⦄, P x → P y → (f x ≤ f y ↔ y ≤ x)) :
    f '' {x | Maximal P x} = {x | Minimal (∃ x₀, P x₀ ∧ f x₀ = ·) x} :=
  image_monotone_setOf_maximal (β := βᵒᵈ) (fun _ _ hx hy ↦ hf hy hx)
Image of Maximal Elements under Antitone Function Equals Minimal Elements of Image Predicate
Informal description
Let $P$ be a predicate on a partially ordered type $\alpha$, and let $f : \alpha \to \beta$ be a function such that for all $x, y$ satisfying $P$, $f(x) \leq f(y)$ if and only if $y \leq x$. Then the image under $f$ of the set of maximal elements of $P$ is equal to the set of minimal elements of the predicate "there exists $x_0$ such that $P(x_0)$ and $f(x_0) = x$".
image_monotone_setOf_minimal_mem theorem
(hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)) : f '' {x | Minimal (· ∈ s) x} = {x | Minimal (· ∈ f '' s) x}
Full source 
theorem image_monotone_setOf_minimal_mem (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)) :
    f '' {x | Minimal (· ∈ s) x} = {x | Minimal (· ∈ f '' s) x} :=
  image_monotone_setOf_minimal hf
Image of Minimal Elements under Monotone Function Preserves Minimality
Informal description
Let $s$ be a set in a partially ordered type $\alpha$, and let $f : \alpha \to \beta$ be a function such that for all $x, y \in s$, $f(x) \leq f(y)$ if and only if $x \leq y$. Then the image under $f$ of the set of minimal elements of $s$ is equal to the set of minimal elements of the image $f(s)$.
image_monotone_setOf_maximal_mem theorem
(hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)) : f '' {x | Maximal (· ∈ s) x} = {x | Maximal (· ∈ f '' s) x}
Full source 
theorem image_monotone_setOf_maximal_mem (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)) :
    f '' {x | Maximal (· ∈ s) x} = {x | Maximal (· ∈ f '' s) x} :=
  image_monotone_setOf_maximal hf
Image of Maximal Elements under Order-Preserving Function Preserves Maximality
Informal description
Let $s$ be a subset of a partially ordered type $\alpha$, and let $f : \alpha \to \beta$ be a function such that for all $x, y \in s$, $f(x) \leq f(y)$ if and only if $x \leq y$. Then the image under $f$ of the set of maximal elements of $s$ is equal to the set of maximal elements of the image $f(s)$.
image_antitone_setOf_minimal_mem theorem
(hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ y ≤ x)) : f '' {x | Minimal (· ∈ s) x} = {x | Maximal (· ∈ f '' s) x}
Full source 
theorem image_antitone_setOf_minimal_mem (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ y ≤ x)) :
    f '' {x | Minimal (· ∈ s) x} = {x | Maximal (· ∈ f '' s) x} :=
  image_antitone_setOf_minimal hf
Minimal Elements Map to Maximal Elements under Antitone Function
Informal description
Let $s$ be a set in a partially ordered type $\alpha$, and let $f : \alpha \to \beta$ be a function such that for all $x, y \in s$, $f(x) \leq f(y)$ if and only if $y \leq x$. Then the image under $f$ of the set of minimal elements of $s$ is equal to the set of maximal elements of the image $f(s)$.
image_antitone_setOf_maximal_mem theorem
(hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ y ≤ x)) : f '' {x | Maximal (· ∈ s) x} = {x | Minimal (· ∈ f '' s) x}
Full source 
theorem image_antitone_setOf_maximal_mem (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ y ≤ x)) :
    f '' {x | Maximal (· ∈ s) x} = {x | Minimal (· ∈ f '' s) x} :=
  image_antitone_setOf_maximal hf
Maximal Elements Map to Minimal Elements under Antitone Function
Informal description
Let $s$ be a subset of a partially ordered type $\alpha$, and let $f \colon \alpha \to \beta$ be a function such that for all $x, y \in s$, the inequality $f(x) \leq f(y)$ holds if and only if $y \leq x$. Then the image under $f$ of the set of maximal elements of $s$ is equal to the set of minimal elements of the image $f(s)$.
OrderEmbedding.minimal_mem_image theorem
(f : α ↪o β) (hx : Minimal (· ∈ s) x) : Minimal (· ∈ f '' s) (f x)
Full source 
theorem minimal_mem_image (f : α ↪o β) (hx : Minimal (· ∈ s) x) : Minimal (· ∈ f '' s) (f x) :=
  _root_.minimal_mem_image_monotone (by simp [f.le_iff_le]) hx
Minimality Preservation under Order Embedding
Informal description
Let $f \colon \alpha \hookrightarrow \beta$ be an order embedding between partially ordered types, and let $s \subseteq \alpha$. If $x \in s$ is a minimal element of $s$ (i.e., there is no $y \in s$ such that $y < x$), then $f(x)$ is a minimal element of the image $f(s) \subseteq \beta$.
OrderEmbedding.maximal_mem_image theorem
(f : α ↪o β) (hx : Maximal (· ∈ s) x) : Maximal (· ∈ f '' s) (f x)
Full source 
theorem maximal_mem_image (f : α ↪o β) (hx : Maximal (· ∈ s) x) : Maximal (· ∈ f '' s) (f x) :=
  _root_.maximal_mem_image_monotone (by simp [f.le_iff_le]) hx
Maximality Preservation under Order Embedding
Informal description
Let $f \colon \alpha \hookrightarrow \beta$ be an order embedding between partially ordered types, and let $s \subseteq \alpha$. If $x \in s$ is a maximal element of $s$ (i.e., there is no $y \in s$ such that $x < y$), then $f(x)$ is a maximal element of the image $f(s) \subseteq \beta$.
OrderEmbedding.minimal_mem_image_iff theorem
(ha : a ∈ s) : Minimal (· ∈ f '' s) (f a) ↔ Minimal (· ∈ s) a
Full source 
theorem minimal_mem_image_iff (ha : a ∈ s) : MinimalMinimal (· ∈ f '' s) (f a) ↔ Minimal (· ∈ s) a :=
  _root_.minimal_mem_image_monotone_iff ha (by simp [f.le_iff_le])
Minimality in Image under Order Embedding iff Minimality in Domain
Informal description
Let $f \colon \alpha \hookrightarrow \beta$ be an order embedding between partially ordered types, and let $s \subseteq \alpha$ with $a \in s$. Then $f(a)$ is a minimal element of the image $f(s) \subseteq \beta$ if and only if $a$ is a minimal element of $s$.
OrderEmbedding.maximal_mem_image_iff theorem
(ha : a ∈ s) : Maximal (· ∈ f '' s) (f a) ↔ Maximal (· ∈ s) a
Full source 
theorem maximal_mem_image_iff (ha : a ∈ s) : MaximalMaximal (· ∈ f '' s) (f a) ↔ Maximal (· ∈ s) a :=
  _root_.maximal_mem_image_monotone_iff ha (by simp [f.le_iff_le])
Maximality in Image under Order Embedding iff Maximality in Domain
Informal description
Let $f \colon \alpha \hookrightarrow \beta$ be an order embedding between partially ordered types, and let $s \subseteq \alpha$ with $a \in s$. Then $f(a)$ is a maximal element of the image $f(s) \subseteq \beta$ if and only if $a$ is a maximal element of $s$.
OrderEmbedding.minimal_apply_mem_inter_range_iff theorem
: Minimal (· ∈ t ∩ range f) (f x) ↔ Minimal (fun x ↦ f x ∈ t) x
Full source 
theorem minimal_apply_mem_inter_range_iff :
    MinimalMinimal (· ∈ t ∩ range f) (f x) ↔ Minimal (fun x ↦ f x ∈ t) x := by
  refine ⟨fun h ↦ ⟨h.prop.1, fun y hy ↦ ?_⟩, fun h ↦ ⟨⟨h.prop, by simp⟩, ?_⟩⟩
  · rw [← f.le_iff_le, ← f.le_iff_le]
    exact h.le_of_le ⟨hy, by simp⟩
  rintro _ ⟨hyt, ⟨y, rfl⟩⟩
  simp_rw [f.le_iff_le]
  exact h.le_of_le hyt
Minimality under Order Embedding and Intersection with Range
Informal description
Let $f : \alpha \hookrightarrow \beta$ be an order embedding between preordered types, $t$ a subset of $\beta$, and $x \in \alpha$. Then $f(x)$ is minimal in $t \cap \mathrm{range}(f)$ if and only if $x$ is minimal with respect to the predicate $\lambda x, f(x) \in t$.
OrderEmbedding.maximal_apply_mem_inter_range_iff theorem
: Maximal (· ∈ t ∩ range f) (f x) ↔ Maximal (fun x ↦ f x ∈ t) x
Full source 
theorem maximal_apply_mem_inter_range_iff :
    MaximalMaximal (· ∈ t ∩ range f) (f x) ↔ Maximal (fun x ↦ f x ∈ t) x :=
  f.dual.minimal_apply_mem_inter_range_iff
Maximality under Order Embedding and Intersection with Range
Informal description
Let $f : \alpha \hookrightarrow \beta$ be an order embedding between preordered types, $t$ a subset of $\beta$, and $x \in \alpha$. Then $f(x)$ is maximal in $t \cap \mathrm{range}(f)$ if and only if $x$ is maximal with respect to the predicate $\lambda x, f(x) \in t$.
OrderEmbedding.minimal_apply_mem_iff theorem
(ht : t ⊆ Set.range f) : Minimal (· ∈ t) (f x) ↔ Minimal (fun x ↦ f x ∈ t) x
Full source 
theorem minimal_apply_mem_iff (ht : t ⊆ Set.range f) :
    MinimalMinimal (· ∈ t) (f x) ↔ Minimal (fun x ↦ f x ∈ t) x := by
  rw [← f.minimal_apply_mem_inter_range_iff, inter_eq_self_of_subset_left ht]
Minimality under Order Embedding and Range Condition
Informal description
Let $f : \alpha \hookrightarrow \beta$ be an order embedding between preordered types, $t$ a subset of $\beta$ contained in the range of $f$, and $x \in \alpha$. Then $f(x)$ is minimal in $t$ if and only if $x$ is minimal with respect to the predicate $\lambda x, f(x) \in t$.
OrderEmbedding.maximal_apply_iff theorem
(ht : t ⊆ Set.range f) : Maximal (· ∈ t) (f x) ↔ Maximal (fun x ↦ f x ∈ t) x
Full source 
theorem maximal_apply_iff (ht : t ⊆ Set.range f) :
    MaximalMaximal (· ∈ t) (f x) ↔ Maximal (fun x ↦ f x ∈ t) x :=
  f.dual.minimal_apply_mem_iff ht
Maximality under Order Embedding and Range Condition
Informal description
Let $f : \alpha \hookrightarrow \beta$ be an order embedding between preordered types, $t$ a subset of $\beta$ contained in the range of $f$, and $x \in \alpha$. Then $f(x)$ is maximal in $t$ if and only if $x$ is maximal with respect to the predicate $\lambda x, f(x) \in t$.
OrderEmbedding.image_setOf_minimal theorem
: f '' {x | Minimal (· ∈ s) x} = {x | Minimal (· ∈ f '' s) x}
Full source 
@[simp] theorem image_setOf_minimal : f '' {x | Minimal (· ∈ s) x} = {x | Minimal (· ∈ f '' s) x} :=
  _root_.image_monotone_setOf_minimal (by simp [f.le_iff_le])
Image of Minimal Elements under Order Embedding Equals Minimal Elements of Image
Informal description
Let $f : \alpha \hookrightarrow \beta$ be an order embedding between partially ordered types, and let $s \subseteq \alpha$. Then the image under $f$ of the set of minimal elements of $s$ is equal to the set of minimal elements of the image $f(s)$.
OrderEmbedding.image_setOf_maximal theorem
: f '' {x | Maximal (· ∈ s) x} = {x | Maximal (· ∈ f '' s) x}
Full source 
@[simp] theorem image_setOf_maximal : f '' {x | Maximal (· ∈ s) x} = {x | Maximal (· ∈ f '' s) x} :=
  _root_.image_monotone_setOf_maximal (by simp [f.le_iff_le])
Image of Maximal Elements under Order Embedding Equals Maximal Elements of Image
Informal description
Let $f : \alpha \hookrightarrow \beta$ be an order embedding between partially ordered types, and let $s \subseteq \alpha$. Then the image under $f$ of the set of maximal elements of $s$ is equal to the set of maximal elements of the image $f(s)$.
OrderEmbedding.inter_preimage_setOf_minimal_eq_of_subset theorem
(hts : t ⊆ f '' s) : x ∈ s ∩ f ⁻¹' {y | Minimal (· ∈ t) y} ↔ Minimal (· ∈ s ∩ f ⁻¹' t) x
Full source 
theorem inter_preimage_setOf_minimal_eq_of_subset (hts : t ⊆ f '' s) :
    x ∈ s ∩ f ⁻¹' {y | Minimal (· ∈ t) y}x ∈ s ∩ f ⁻¹' {y | Minimal (· ∈ t) y} ↔ Minimal (· ∈ s ∩ f ⁻¹' t) x := by
  simp_rw [mem_inter_iff, preimage_setOf_eq, mem_setOf_eq, mem_preimage,
    f.minimal_apply_mem_iff (hts.trans (image_subset_range _ _)),
    minimal_and_iff_left_of_imp (fun _ hx ↦ f.injective.mem_set_image.1 <| hts hx)]
Minimality under Order Embedding via Preimage and Intersection
Informal description
Let $f : \alpha \hookrightarrow \beta$ be an order embedding between preordered types, $s \subseteq \alpha$, and $t \subseteq \beta$ such that $t \subseteq f(s)$. For any $x \in \alpha$, the following are equivalent: 1. $x$ belongs to $s$ and $f(x)$ is minimal in $t$; 2. $x$ is minimal in the set $s \cap f^{-1}(t)$.
OrderEmbedding.inter_preimage_setOf_maximal_eq_of_subset theorem
(hts : t ⊆ f '' s) : x ∈ s ∩ f ⁻¹' {y | Maximal (· ∈ t) y} ↔ Maximal (· ∈ s ∩ f ⁻¹' t) x
Full source 
theorem inter_preimage_setOf_maximal_eq_of_subset (hts : t ⊆ f '' s) :
    x ∈ s ∩ f ⁻¹' {y | Maximal (· ∈ t) y}x ∈ s ∩ f ⁻¹' {y | Maximal (· ∈ t) y} ↔ Maximal (· ∈ s ∩ f ⁻¹' t) x :=
  f.dual.inter_preimage_setOf_minimal_eq_of_subset hts
Maximality under Order Embedding via Preimage and Intersection
Informal description
Let $f : \alpha \hookrightarrow \beta$ be an order embedding between preordered types, $s \subseteq \alpha$, and $t \subseteq \beta$ such that $t \subseteq f(s)$. For any $x \in \alpha$, the following are equivalent: 1. $x$ belongs to $s$ and $f(x)$ is maximal in $t$; 2. $x$ is maximal in the set $s \cap f^{-1}(t)$.
OrderIso.image_setOf_minimal theorem
(f : α ≃o β) (P : α → Prop) : f '' {x | Minimal P x} = {x | Minimal (fun x ↦ P (f.symm x)) x}
Full source 
theorem image_setOf_minimal (f : α ≃o β) (P : α → Prop) :
    f '' {x | Minimal P x} = {x | Minimal (fun x ↦ P (f.symm x)) x} := by
  convert _root_.image_monotone_setOf_minimal (f := f) (by simp [f.le_iff_le])
  aesop
Image of Minimal Elements under Order Isomorphism
Informal description
Let $\alpha$ and $\beta$ be preordered types, and let $f : \alpha \simeq_o \beta$ be an order isomorphism between them. For any predicate $P$ on $\alpha$, the image under $f$ of the set of minimal elements of $P$ is equal to the set of minimal elements of the predicate $P \circ f^{-1}$ on $\beta$. In other words, $$ f(\{x \in \alpha \mid \text{$x$ is minimal for $P$}\}) = \{y \in \beta \mid \text{$y$ is minimal for $P(f^{-1}(y))$}\}. $$
OrderIso.image_setOf_maximal theorem
(f : α ≃o β) (P : α → Prop) : f '' {x | Maximal P x} = {x | Maximal (fun x ↦ P (f.symm x)) x}
Full source 
theorem image_setOf_maximal (f : α ≃o β) (P : α → Prop) :
    f '' {x | Maximal P x} = {x | Maximal (fun x ↦ P (f.symm x)) x} := by
  convert _root_.image_monotone_setOf_maximal (f := f) (by simp [f.le_iff_le])
  aesop
Image of Maximal Elements under Order Isomorphism
Informal description
Let $\alpha$ and $\beta$ be preordered types, and let $f : \alpha \simeq_o \beta$ be an order isomorphism between them. For any predicate $P$ on $\alpha$, the image under $f$ of the set of maximal elements of $P$ is equal to the set of maximal elements of the predicate $P \circ f^{-1}$ on $\beta$. In other words, $$ f(\{x \in \alpha \mid \text{$x$ is maximal for $P$}\}) = \{y \in \beta \mid \text{$y$ is maximal for $P(f^{-1}(y))$}\}. $$
OrderIso.map_minimal_mem theorem
(f : s ≃o t) (hx : Minimal (· ∈ s) x) : Minimal (· ∈ t) (f ⟨x, hx.prop⟩)
Full source 
theorem map_minimal_mem (f : s ≃o t) (hx : Minimal (· ∈ s) x) :
    Minimal (· ∈ t) (f ⟨x, hx.prop⟩) := by
  simpa only [show t = range (Subtype.valSubtype.val ∘ f) by simp, mem_univ, minimal_true_subtype, hx,
    true_imp_iff, image_univ] using OrderEmbedding.minimal_mem_image
    (f.toOrderEmbedding.trans (OrderEmbedding.subtype t)) (s := univ) (x := ⟨x, hx.prop⟩)
Minimality Preservation under Order Isomorphism
Informal description
Let $s$ and $t$ be sets with order structures, and let $f : s \simeq_o t$ be an order isomorphism between them. If $x \in s$ is a minimal element of $s$ (i.e., there is no $y \in s$ such that $y < x$), then the image $f(x) \in t$ is a minimal element of $t$.
OrderIso.map_maximal_mem theorem
(f : s ≃o t) (hx : Maximal (· ∈ s) x) : Maximal (· ∈ t) (f ⟨x, hx.prop⟩)
Full source 
theorem map_maximal_mem (f : s ≃o t) (hx : Maximal (· ∈ s) x) :
    Maximal (· ∈ t) (f ⟨x, hx.prop⟩) := by
  simpa only [show t = range (Subtype.valSubtype.val ∘ f) by simp, mem_univ, maximal_true_subtype, hx,
    true_imp_iff, image_univ] using OrderEmbedding.maximal_mem_image
    (f.toOrderEmbedding.trans (OrderEmbedding.subtype t)) (s := univ) (x := ⟨x, hx.prop⟩)
Maximality Preservation under Order Isomorphism
Informal description
Let $s$ and $t$ be sets with order structures, and let $f : s \simeq_o t$ be an order isomorphism between them. If $x \in s$ is a maximal element of $s$ (i.e., there is no $y \in s$ such that $x < y$), then the image $f(x) \in t$ is a maximal element of $t$.
OrderIso.mapSetOfMinimal definition
(f : s ≃o t) : {x | Minimal (· ∈ s) x} ≃o {x | Minimal (· ∈ t) x}
Full source 
/-- If two sets are order isomorphic, their minimals are also order isomorphic. -/
def mapSetOfMinimal (f : s ≃o t) : {x | Minimal (· ∈ s) x}{x | Minimal (· ∈ s) x} ≃o {x | Minimal (· ∈ t) x} where
  toFun x := ⟨f ⟨x, x.2.1⟩, f.map_minimal_mem x.2⟩
  invFun x := ⟨f.symm ⟨x, x.2.1⟩, f.symm.map_minimal_mem x.2⟩
  left_inv x := Subtype.ext (congr_arg Subtype.val <| f.left_inv ⟨x, x.2.1⟩ :)
  right_inv x := Subtype.ext (congr_arg Subtype.val <| f.right_inv ⟨x, x.2.1⟩ :)
  map_rel_iff' := f.map_rel_iff
Order isomorphism preserves minimal elements
Informal description
Given an order isomorphism \( f : s \simeq_o t \) between two sets \( s \) and \( t \) with order structures, the function maps the set of minimal elements of \( s \) to the set of minimal elements of \( t \) in an order-preserving manner. Specifically, for any minimal element \( x \) in \( s \), the image \( f(x) \) is a minimal element in \( t \), and this correspondence is bijective and preserves the order relation.
OrderIso.mapSetOfMaximal definition
(f : s ≃o t) : {x | Maximal (· ∈ s) x} ≃o {x | Maximal (· ∈ t) x}
Full source 
/-- If two sets are order isomorphic, their maximals are also order isomorphic. -/
def mapSetOfMaximal (f : s ≃o t) : {x | Maximal (· ∈ s) x}{x | Maximal (· ∈ s) x} ≃o {x | Maximal (· ∈ t) x} where
  toFun x := ⟨f ⟨x, x.2.1⟩, f.map_maximal_mem x.2⟩
  invFun x := ⟨f.symm ⟨x, x.2.1⟩, f.symm.map_maximal_mem x.2⟩
  left_inv x := Subtype.ext (congr_arg Subtype.val <| f.left_inv ⟨x, x.2.1⟩ :)
  right_inv x := Subtype.ext (congr_arg Subtype.val <| f.right_inv ⟨x, x.2.1⟩ :)
  map_rel_iff' := f.map_rel_iff
Order isomorphism preserves maximal elements
Informal description
Given an order isomorphism $f : s \simeq_o t$ between two sets $s$ and $t$ with order structures, the function maps the set of maximal elements of $s$ to the set of maximal elements of $t$ in an order-preserving manner. Specifically, for any maximal element $x$ in $s$, the image $f(x)$ is maximal in $t$, and this correspondence forms an order isomorphism between the sets of maximal elements of $s$ and $t$.
OrderIso.setOfMinimalIsoSetOfMaximal definition
(f : s ≃o tᵒᵈ) : {x | Minimal (· ∈ s) x} ≃o {x | Maximal (· ∈ t) (ofDual x)}
Full source 
/-- If two sets are antitonically order isomorphic, their minimals/maximals are too. -/
def setOfMinimalIsoSetOfMaximal (f : s ≃o tᵒᵈ) :
    {x | Minimal (· ∈ s) x}{x | Minimal (· ∈ s) x} ≃o {x | Maximal (· ∈ t) (ofDual x)} where
      toFun x := ⟨(f ⟨x.1, x.2.1⟩).1, ((show s ≃o ofDual ⁻¹' t from f).mapSetOfMinimal x).2⟩
      invFun x := ⟨(f.symm ⟨x.1, x.2.1⟩).1,
        ((show ofDual ⁻¹' t ≃o s from f.symm).mapSetOfMinimal x).2⟩
      __ := (show s ≃o ofDual⁻¹' t from f).mapSetOfMinimal
Order isomorphism between minimal elements and maximal elements under order duality
Informal description
Given an order isomorphism \( f : s \simeq_o t^\mathrm{op} \) between a set \( s \) and the dual order of a set \( t \), the function induces an order isomorphism between the set of minimal elements of \( s \) and the set of maximal elements of \( t \). Specifically, for any minimal element \( x \) in \( s \), the image \( f(x) \) is a maximal element in \( t \), and this correspondence is bijective and order-preserving.
OrderIso.setOfMaximalIsoSetOfMinimal definition
(f : s ≃o tᵒᵈ) : {x | Maximal (· ∈ s) x} ≃o {x | Minimal (· ∈ t) (ofDual x)}
Full source 
/-- If two sets are antitonically order isomorphic, their maximals/minimals are too. -/
def setOfMaximalIsoSetOfMinimal (f : s ≃o tᵒᵈ) :
    {x | Maximal (· ∈ s) x}{x | Maximal (· ∈ s) x} ≃o {x | Minimal (· ∈ t) (ofDual x)} where
  toFun x := ⟨(f ⟨x.1, x.2.1⟩).1, ((show s ≃o ofDual ⁻¹' t from f).mapSetOfMaximal x).2⟩
  invFun x := ⟨(f.symm ⟨x.1, x.2.1⟩).1,
        ((show ofDual ⁻¹' t ≃o s from f.symm).mapSetOfMaximal x).2⟩
  __ := (show s ≃o ofDual⁻¹' t from f).mapSetOfMaximal
Order isomorphism between maximal elements and minimal elements under duality
Informal description
Given an order isomorphism $f : s \simeq_o t^{\mathrm{op}}$ between a set $s$ and the dual order of a set $t$, the function maps the set of maximal elements of $s$ to the set of minimal elements of $t$ in an order-preserving manner. Specifically, for any maximal element $x$ in $s$, the image $f(x)$ is minimal in $t$, and this correspondence forms an order isomorphism between the sets of maximal elements of $s$ and minimal elements of $t$.
minimal_mem_Icc theorem
(hab : a ≤ b) : Minimal (· ∈ Icc a b) x ↔ x = a
Full source 
theorem minimal_mem_Icc (hab : a ≤ b) : MinimalMinimal (· ∈ Icc a b) x ↔ x = a :=
  minimal_iff_eq ⟨rfl.le, hab⟩ (fun _ ↦ And.left)
Minimal Element Characterization in Closed Interval: $x$ is minimal in $[a, b]$ iff $x = a$
Informal description
For any elements $a$ and $b$ in a preorder with $a \leq b$, an element $x$ is minimal in the closed interval $[a, b]$ if and only if $x = a$.
maximal_mem_Icc theorem
(hab : a ≤ b) : Maximal (· ∈ Icc a b) x ↔ x = b
Full source 
theorem maximal_mem_Icc (hab : a ≤ b) : MaximalMaximal (· ∈ Icc a b) x ↔ x = b :=
  maximal_iff_eq ⟨hab, rfl.le⟩ (fun _ ↦ And.right)
Maximal Element Characterization in Closed Interval: $x$ is maximal in $[a, b]$ iff $x = b$
Informal description
For any elements $a$ and $b$ in a preorder with $a \leq b$, an element $x$ is maximal in the closed interval $[a, b]$ if and only if $x = b$.