Mathlib.Order.BoundedOrder.Monotone

StrictMono.apply_eq_top_iff theorem

(hf : StrictMono f) : f a = f ⊤ ↔ a = ⊤

Full source

theorem StrictMono.apply_eq_top_iff (hf : StrictMono f) : f a = f ⊤ ↔ a = ⊤ :=
  ⟨fun h => not_lt_top_iff.1 fun ha => (hf ha).ne h, congr_arg _⟩

Strictly monotone function preserves top equality

Informal description

Let $f : \alpha \to \beta$ be a strictly monotone function between partial orders, where $\beta$ has a top element $\top$. Then for any element $a \in \alpha$, we have $f(a) = f(\top)$ if and only if $a = \top$.

StrictAnti.apply_eq_top_iff theorem

(hf : StrictAnti f) : f a = f ⊤ ↔ a = ⊤

Full source

theorem StrictAnti.apply_eq_top_iff (hf : StrictAnti f) : f a = f ⊤ ↔ a = ⊤ :=
  ⟨fun h => not_lt_top_iff.1 fun ha => (hf ha).ne' h, congr_arg _⟩

Strictly Antitone Function Preserves Top Element Equality

Informal description

For a strictly antitone function $f$ from a partially ordered set to a partially ordered set with a top element $\top$, the equality $f(a) = f(\top)$ holds if and only if $a = \top$.

StrictMono.maximal_preimage_top theorem

 [LinearOrder α] [Preorder β] [OrderTop β] {f : α → β} (H : StrictMono f) {a} (h_top : f a = ⊤) (x : α) : x ≤ a

Full source

theorem StrictMono.maximal_preimage_top [LinearOrder α] [Preorder β] [OrderTop β] {f : α → β}
    (H : StrictMono f) {a} (h_top : f a = ⊤) (x : α) : x ≤ a :=
  H.maximal_of_maximal_image
    (fun p => by
      rw [h_top]
      exact le_top)
    x

Maximal Preimage of Top Element under Strictly Monotone Function

Informal description

Let $\alpha$ be a linearly ordered type and $\beta$ be a preordered type with a top element $\top$. Given a strictly monotone function $f \colon \alpha \to \beta$ and an element $a \in \alpha$ such that $f(a) = \top$, then for any $x \in \alpha$, we have $x \leq a$.

StrictMono.apply_eq_bot_iff theorem

(hf : StrictMono f) : f a = f ⊥ ↔ a = ⊥

Full source

theorem StrictMono.apply_eq_bot_iff (hf : StrictMono f) : f a = f ⊥ ↔ a = ⊥ :=
  hf.dual.apply_eq_top_iff

Strictly monotone function preserves bottom equality

Informal description

Let $f : \alpha \to \beta$ be a strictly monotone function between partial orders, where $\beta$ has a bottom element $\bot$. Then for any element $a \in \alpha$, we have $f(a) = f(\bot)$ if and only if $a = \bot$.

StrictAnti.apply_eq_bot_iff theorem

(hf : StrictAnti f) : f a = f ⊥ ↔ a = ⊥

Full source

theorem StrictAnti.apply_eq_bot_iff (hf : StrictAnti f) : f a = f ⊥ ↔ a = ⊥ :=
  hf.dual.apply_eq_top_iff

Strictly Antitone Function Preserves Bottom Element Equality

Informal description

For a strictly antitone function $f$ from a partially ordered set to a partially ordered set with a bottom element $\bot$, the equality $f(a) = f(\bot)$ holds if and only if $a = \bot$.

StrictMono.minimal_preimage_bot theorem

 [LinearOrder α] [Preorder β] [OrderBot β] {f : α → β} (H : StrictMono f) {a} (h_bot : f a = ⊥) (x : α) : a ≤ x

Full source

theorem StrictMono.minimal_preimage_bot [LinearOrder α] [Preorder β] [OrderBot β] {f : α → β}
    (H : StrictMono f) {a} (h_bot : f a = ⊥) (x : α) : a ≤ x :=
  H.minimal_of_minimal_image
    (fun p => by
      rw [h_bot]
      exact bot_le)
    x

Minimal Preimage of Bottom Element under Strictly Monotone Function

Informal description

Let $\alpha$ be a linearly ordered type and $\beta$ be a preordered type with a bottom element $\bot$. Given a strictly monotone function $f : \alpha \to \beta$ and an element $a \in \alpha$ such that $f(a) = \bot$, then $a$ is the minimal element in $\alpha$ with respect to the order, i.e., $a \leq x$ for all $x \in \alpha$.

monotone_and theorem

{p q : α → Prop} (m_p : Monotone p) (m_q : Monotone q) : Monotone fun x => p x ∧ q x

Full source

theorem monotone_and {p q : α → Prop} (m_p : Monotone p) (m_q : Monotone q) :
    Monotone fun x => p x ∧ q x :=
  fun _ _ h => And.imp (m_p h) (m_q h)

Monotonicity of Conjunction of Monotone Predicates

Informal description

Let $p, q : \alpha \to \mathrm{Prop}$ be monotone predicates on a partially ordered type $\alpha$. Then the predicate $x \mapsto p(x) \land q(x)$ is also monotone.

monotone_or theorem

{p q : α → Prop} (m_p : Monotone p) (m_q : Monotone q) : Monotone fun x => p x ∨ q x

Full source

theorem monotone_or {p q : α → Prop} (m_p : Monotone p) (m_q : Monotone q) :
    Monotone fun x => p x ∨ q x :=
  fun _ _ h => Or.imp (m_p h) (m_q h)

Monotonicity is preserved under disjunction

Informal description

Let $p, q : \alpha \to \mathrm{Prop}$ be monotone functions from a partially ordered set $\alpha$ to propositions. Then the function $x \mapsto p(x) \lor q(x)$ is also monotone.

monotone_le theorem

{x : α} : Monotone (x ≤ ·)

Full source

theorem monotone_le {x : α} : Monotone (x ≤ ·) := fun _ _ h' h => h.trans h'

Monotonicity of the "greater than or equal to" predicate

Informal description

For any element $x$ in a partially ordered set $\alpha$, the function $y \mapsto (x \leq y)$ is monotone.

monotone_lt theorem

{x : α} : Monotone (x < ·)

Full source

theorem monotone_lt {x : α} : Monotone (x < ·) := fun _ _ h' h => h.trans_le h'

Monotonicity of strict lower sets: $y \mapsto x < y$ is monotone

Informal description

For any element $x$ in a partially ordered set $\alpha$, the function $y \mapsto x < y$ is monotone.

antitone_le theorem

{x : α} : Antitone (· ≤ x)

Full source

theorem antitone_le {x : α} : Antitone (· ≤ x) := fun _ _ h' h => h'.trans h

Antitonicity of the "Less Than or Equal To" Predicate

Informal description

For any element $x$ in a partially ordered type $\alpha$, the function $\lambda y, y \leq x$ is antitone, meaning that if $y_1 \leq y_2$, then $y_2 \leq x$ implies $y_1 \leq x$.

antitone_lt theorem

{x : α} : Antitone (· < x)

Full source

theorem antitone_lt {x : α} : Antitone (· < x) := fun _ _ h' h => h'.trans_lt h

Antitonicity of the Strict Less-Than Relation with Fixed Right Argument

Informal description

For any element $x$ in a type $\alpha$ with a strict order relation $<$, the function $(\cdot < x)$ is antitone, meaning that for any $y_1, y_2 \in \alpha$, if $y_1 \leq y_2$, then $(y_2 < x) \to (y_1 < x)$.

Monotone.forall theorem

{P : β → α → Prop} (hP : ∀ x, Monotone (P x)) : Monotone fun y => ∀ x, P x y

Full source

theorem Monotone.forall {P : β → α → Prop} (hP : ∀ x, Monotone (P x)) :
    Monotone fun y => ∀ x, P x y :=
  fun _ _ hy h x => hP x hy <| h x

Monotonicity of Universal Quantification over Monotone Predicates

Informal description

Let $P : \beta \to \alpha \to \text{Prop}$ be a family of predicates such that for each $x \in \beta$, the predicate $P(x)$ is monotone in its second argument. Then the predicate $\forall x, P(x, y)$ is also monotone in $y$.

Antitone.forall theorem

{P : β → α → Prop} (hP : ∀ x, Antitone (P x)) : Antitone fun y => ∀ x, P x y

Full source

theorem Antitone.forall {P : β → α → Prop} (hP : ∀ x, Antitone (P x)) :
    Antitone fun y => ∀ x, P x y :=
  fun _ _ hy h x => hP x hy (h x)

Universal Quantification Preserves Antitonicity

Informal description

Let $P : \beta \to \alpha \to \text{Prop}$ be a family of predicates such that for each $x \in \beta$, the predicate $P(x) : \alpha \to \text{Prop}$ is antitone (i.e., for all $y_1 \leq y_2$ in $\alpha$, $P(x)(y_2) \to P(x)(y_1)$). Then the predicate $\forall x, P(x) : \alpha \to \text{Prop}$ is also antitone.

Monotone.ball theorem

{P : β → α → Prop} {s : Set β} (hP : ∀ x ∈ s, Monotone (P x)) : Monotone fun y => ∀ x ∈ s, P x y

Full source

theorem Monotone.ball {P : β → α → Prop} {s : Set β} (hP : ∀ x ∈ s, Monotone (P x)) :
    Monotone fun y => ∀ x ∈ s, P x y := fun _ _ hy h x hx => hP x hx hy (h x hx)

Monotonicity of Universal Quantification over a Set

Informal description

Let $P : \beta \to \alpha \to \text{Prop}$ be a family of predicates indexed by $\beta$ and $\alpha$, and let $s$ be a subset of $\beta$. If for every $x \in s$, the predicate $P(x, \cdot)$ is monotone in its second argument, then the predicate $\forall x \in s, P(x, y)$ is also monotone in $y$.

Antitone.ball theorem

{P : β → α → Prop} {s : Set β} (hP : ∀ x ∈ s, Antitone (P x)) : Antitone fun y => ∀ x ∈ s, P x y

Full source

theorem Antitone.ball {P : β → α → Prop} {s : Set β} (hP : ∀ x ∈ s, Antitone (P x)) :
    Antitone fun y => ∀ x ∈ s, P x y := fun _ _ hy h x hx => hP x hx hy (h x hx)

Antitone Property of Universal Quantification over a Set

Informal description

Let $P : \beta \to \alpha \to \text{Prop}$ be a family of predicates and $s$ be a subset of $\beta$. If for every $x \in s$, the predicate $P(x)$ is antitone in its second argument (i.e., $P(x) : \alpha \to \text{Prop}$ is antitone), then the predicate $\forall x \in s, P(x, y)$ is also antitone in $y$.

Monotone.exists theorem

{P : β → α → Prop} (hP : ∀ x, Monotone (P x)) : Monotone fun y => ∃ x, P x y

Full source

theorem Monotone.exists {P : β → α → Prop} (hP : ∀ x, Monotone (P x)) :
    Monotone fun y => ∃ x, P x y :=
  fun _ _ hy ⟨x, hx⟩ ↦ ⟨x, hP x hy hx⟩

Monotonicity of Existential Quantifier over Monotone Predicates

Informal description

Let $\alpha$ and $\beta$ be types with a partial order on $\alpha$, and let $P : \beta \to \alpha \to \text{Prop}$ be a family of predicates such that for each $x \in \beta$, the predicate $P(x)$ is monotone in its second argument. Then the predicate $\lambda y, \exists x, P(x, y)$ is also monotone in $y$.

Antitone.exists theorem

{P : β → α → Prop} (hP : ∀ x, Antitone (P x)) : Antitone fun y => ∃ x, P x y

Full source

theorem Antitone.exists {P : β → α → Prop} (hP : ∀ x, Antitone (P x)) :
    Antitone fun y => ∃ x, P x y :=
  fun _ _ hy ⟨x, hx⟩ ↦ ⟨x, hP x hy hx⟩

Antitone Property of Existential Quantification over Antitone Predicates

Informal description

Let $P : \beta \to \alpha \to \text{Prop}$ be a family of predicates such that for each $x \in \beta$, the predicate $P(x)$ is antitone in its second argument (i.e., for any $y_1 \leq y_2$ in $\alpha$, $P(x)(y_2) \to P(x)(y_1)$). Then the predicate $\lambda y, \exists x, P(x)(y)$ is also antitone in $y$.

forall_ge_iff theorem

{P : α → Prop} {x₀ : α} (hP : Monotone P) : (∀ x ≥ x₀, P x) ↔ P x₀

Full source

theorem forall_ge_iff {P : α → Prop} {x₀ : α} (hP : Monotone P) :
    (∀ x ≥ x₀, P x) ↔ P x₀ :=
  ⟨fun H ↦ H x₀ le_rfl, fun H _ hx ↦ hP hx H⟩

Universal quantification over upper sets for monotone predicates

Informal description

Let $P : \alpha \to \text{Prop}$ be a monotone function on a preorder $\alpha$, and let $x_0 \in \alpha$. Then the following equivalence holds: \[ (\forall x \geq x_0, P(x)) \leftrightarrow P(x_0). \]

forall_le_iff theorem

{P : α → Prop} {x₀ : α} (hP : Antitone P) : (∀ x ≤ x₀, P x) ↔ P x₀

Full source

theorem forall_le_iff {P : α → Prop} {x₀ : α} (hP : Antitone P) :
    (∀ x ≤ x₀, P x) ↔ P x₀ :=
  ⟨fun H ↦ H x₀ le_rfl, fun H _ hx ↦ hP hx H⟩

Universal quantification over lower set equivalent to value at bound for antitone functions

Informal description

For an antitone function $P \colon \alpha \to \text{Prop}$ and an element $x_0 \in \alpha$, the universal quantification $\forall x \leq x_0, P(x)$ is equivalent to $P(x_0)$.