Mathlib.Data.Set.Order

Set.monotoneOn_iff_monotone theorem

: MonotoneOn f s ↔ Monotone fun a : s => f a

Full source

theorem monotoneOn_iff_monotone : MonotoneOnMonotoneOn f s ↔
    Monotone fun a : s => f a := by
  simp [Monotone, MonotoneOn]

Monotonicity on Set vs. Restricted Function

Informal description

A function $f$ is monotone (monotonically increasing) on a set $s$ if and only if the restriction of $f$ to $s$ is monotone as a function on the subtype $s$.

Set.antitoneOn_iff_antitone theorem

: AntitoneOn f s ↔ Antitone fun a : s => f a

Full source

theorem antitoneOn_iff_antitone : AntitoneOnAntitoneOn f s ↔
    Antitone fun a : s => f a := by
  simp [Antitone, AntitoneOn]

Antitonicity on Set vs. Restricted Function

Informal description

A function $f$ is antitone (monotonically decreasing) on a set $s$ if and only if the restriction of $f$ to $s$ is antitone as a function on the subtype $s$.

Set.strictMonoOn_iff_strictMono theorem

: StrictMonoOn f s ↔ StrictMono fun a : s => f a

Full source

theorem strictMonoOn_iff_strictMono : StrictMonoOnStrictMonoOn f s ↔
    StrictMono fun a : s => f a := by
  simp [StrictMono, StrictMonoOn]

Strictly Increasing Function on Set vs. Restricted Function

Informal description

A function $f$ is strictly increasing on a set $s$ if and only if the restriction of $f$ to $s$ is strictly increasing as a function on the subtype $s$.

Set.strictAntiOn_iff_strictAnti theorem

: StrictAntiOn f s ↔ StrictAnti fun a : s => f a

Full source

theorem strictAntiOn_iff_strictAnti : StrictAntiOnStrictAntiOn f s ↔
    StrictAnti fun a : s => f a := by
  simp [StrictAnti, StrictAntiOn]

Strictly Decreasing Function on Set vs. Restricted Function

Informal description

A function $f$ is strictly decreasing on a set $s$ if and only if the restriction of $f$ to $s$ is strictly decreasing as a function on the subtype $s$.

Set.not_monotoneOn_not_antitoneOn_iff_exists_le_le theorem

 :
  ¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔
    ∃ᵉ (a ∈ s) (b ∈ s) (c ∈ s), a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Full source

/-- A function between linear orders which is neither monotone nor antitone makes a dent upright or
downright. -/
theorem not_monotoneOn_not_antitoneOn_iff_exists_le_le :
    ¬MonotoneOn f s¬MonotoneOn f s ∧ ¬AntitoneOn f s¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔
      ∃ᵉ (a ∈ s) (b ∈ s) (c ∈ s), a ≤ b ∧ b ≤ c ∧
        (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c) := by
  simp [monotoneOn_iff_monotone, antitoneOn_iff_antitone, and_assoc, exists_and_left,
    not_monotone_not_antitone_iff_exists_le_le, @and_left_comm (_ ∈ s)]

Characterization of Non-Monotone and Non-Antitone Functions via Local Extrema

Informal description

A function $f$ defined on a set $s$ in a linear order is neither monotone nor antitone if and only if there exist elements $a, b, c \in s$ with $a \leq b \leq c$ such that either ($f(a) < f(b)$ and $f(c) < f(b)$) or ($f(b) < f(a)$ and $f(b) < f(c)$).

Set.not_monotoneOn_not_antitoneOn_iff_exists_lt_lt theorem

 :
  ¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔
    ∃ᵉ (a ∈ s) (b ∈ s) (c ∈ s), a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Full source

/-- A function between linear orders which is neither monotone nor antitone makes a dent upright or
downright. -/
theorem not_monotoneOn_not_antitoneOn_iff_exists_lt_lt :
    ¬MonotoneOn f s¬MonotoneOn f s ∧ ¬AntitoneOn f s¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔
      ∃ᵉ (a ∈ s) (b ∈ s) (c ∈ s), a < b ∧ b < c ∧
        (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c) := by
  simp [monotoneOn_iff_monotone, antitoneOn_iff_antitone, and_assoc, exists_and_left,
    not_monotone_not_antitone_iff_exists_lt_lt, @and_left_comm (_ ∈ s)]

Characterization of Non-Monotone Non-Antitone Functions via Local Extrema

Informal description

A function $f$ defined on a set $s$ in a linear order is neither monotone nor antitone if and only if there exist elements $a, b, c \in s$ with $a < b < c$ such that either ($f(a) < f(b)$ and $f(c) < f(b)$) or ($f(b) < f(a)$ and $f(b) < f(c)$).

Monotone.inter theorem

[Preorder β] {f g : β → Set α} (hf : Monotone f) (hg : Monotone g) : Monotone fun x => f x ∩ g x

Full source

theorem Monotone.inter [Preorder β] {f g : β → Set α} (hf : Monotone f) (hg : Monotone g) :
    Monotone fun x => f x ∩ g x :=
  hf.inf hg

Monotonicity of Intersection of Monotone Set-Valued Functions

Informal description

Let $\beta$ be a preorder and $\alpha$ be any type. For any two monotone functions $f, g : \beta \to \text{Set}(\alpha)$, the function $x \mapsto f(x) \cap g(x)$ is also monotone.

MonotoneOn.inter theorem

 [Preorder β] {f g : β → Set α} {s : Set β} (hf : MonotoneOn f s) (hg : MonotoneOn g s) :
  MonotoneOn (fun x => f x ∩ g x) s

Full source

theorem MonotoneOn.inter [Preorder β] {f g : β → Set α} {s : Set β} (hf : MonotoneOn f s)
    (hg : MonotoneOn g s) : MonotoneOn (fun x => f x ∩ g x) s :=
  hf.inf hg

Monotonicity of Intersection of Monotone Set-Valued Functions

Informal description

Let $\beta$ be a preorder and $\alpha$ be any type. Given two functions $f, g \colon \beta \to \text{Set } \alpha$ that are monotone on a subset $s \subseteq \beta$, their pointwise intersection $x \mapsto f(x) \cap g(x)$ is also monotone on $s$.

Antitone.inter theorem

[Preorder β] {f g : β → Set α} (hf : Antitone f) (hg : Antitone g) : Antitone fun x => f x ∩ g x

Full source

theorem Antitone.inter [Preorder β] {f g : β → Set α} (hf : Antitone f) (hg : Antitone g) :
    Antitone fun x => f x ∩ g x :=
  hf.inf hg

Antitonicity of Intersection of Antitone Set-Valued Functions

Informal description

Let $\beta$ be a preorder and $\alpha$ be any type. Given two antitone functions $f, g : \beta \to \text{Set } \alpha$, the function $x \mapsto f(x) \cap g(x)$ is also antitone.

AntitoneOn.inter theorem

 [Preorder β] {f g : β → Set α} {s : Set β} (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
  AntitoneOn (fun x => f x ∩ g x) s

Full source

theorem AntitoneOn.inter [Preorder β] {f g : β → Set α} {s : Set β} (hf : AntitoneOn f s)
    (hg : AntitoneOn g s) : AntitoneOn (fun x => f x ∩ g x) s :=
  hf.inf hg

Intersection of Antitone Set-Valued Functions is Antitone on a Subset

Informal description

Let $\beta$ be a preorder and $\alpha$ be any type. Given two functions $f, g \colon \beta \to \text{Set } \alpha$ that are antitone on a subset $s \subseteq \beta$, the function $x \mapsto f(x) \cap g(x)$ is also antitone on $s$.

Monotone.union theorem

[Preorder β] {f g : β → Set α} (hf : Monotone f) (hg : Monotone g) : Monotone fun x => f x ∪ g x

Full source

theorem Monotone.union [Preorder β] {f g : β → Set α} (hf : Monotone f) (hg : Monotone g) :
    Monotone fun x => f x ∪ g x :=
  hf.sup hg

Monotonicity of Union of Monotone Set-Valued Functions

Informal description

Let $\beta$ be a preorder and $\alpha$ be any type. Given two monotone functions $f, g : \beta \to \text{Set } \alpha$, the function $x \mapsto f(x) \cup g(x)$ is also monotone.

MonotoneOn.union theorem

 [Preorder β] {f g : β → Set α} {s : Set β} (hf : MonotoneOn f s) (hg : MonotoneOn g s) :
  MonotoneOn (fun x => f x ∪ g x) s

Full source

theorem MonotoneOn.union [Preorder β] {f g : β → Set α} {s : Set β} (hf : MonotoneOn f s)
    (hg : MonotoneOn g s) : MonotoneOn (fun x => f x ∪ g x) s :=
  hf.sup hg

Monotonicity of Union of Monotone Set-Valued Functions on a Subset

Informal description

Let $\beta$ be a preorder and $\alpha$ be any type. Given two functions $f, g : \beta \to \text{Set } \alpha$ that are monotone on a subset $s \subseteq \beta$, the function $x \mapsto f(x) \cup g(x)$ is also monotone on $s$.

Antitone.union theorem

[Preorder β] {f g : β → Set α} (hf : Antitone f) (hg : Antitone g) : Antitone fun x => f x ∪ g x

Full source

theorem Antitone.union [Preorder β] {f g : β → Set α} (hf : Antitone f) (hg : Antitone g) :
    Antitone fun x => f x ∪ g x :=
  hf.sup hg

Antitonicity of Union of Antitone Set-Valued Functions

Informal description

Let $\beta$ be a preorder and $\alpha$ be any type. Given two antitone functions $f, g : \beta \to \text{Set } \alpha$, the function $x \mapsto f(x) \cup g(x)$ is also antitone. That is, for any $x, y \in \beta$ with $x \leq y$, we have $f(y) \cup g(y) \subseteq f(x) \cup g(x)$.

AntitoneOn.union theorem

 [Preorder β] {f g : β → Set α} {s : Set β} (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
  AntitoneOn (fun x => f x ∪ g x) s

Full source

theorem AntitoneOn.union [Preorder β] {f g : β → Set α} {s : Set β} (hf : AntitoneOn f s)
    (hg : AntitoneOn g s) : AntitoneOn (fun x => f x ∪ g x) s :=
  hf.sup hg

Union of Antitone Set-Valued Functions is Antitone on a Subset

Informal description

Let $\beta$ be a preordered set and $\alpha$ be any type. Given two set-valued functions $f, g : \beta \to \text{Set } \alpha$ that are antitone on a subset $s \subseteq \beta$, the function $x \mapsto f(x) \cup g(x)$ is also antitone on $s$.

Set.monotone_setOf theorem

[Preorder α] {p : α → β → Prop} (hp : ∀ b, Monotone fun a => p a b) : Monotone fun a => {b | p a b}

Full source

theorem monotone_setOf [Preorder α] {p : α → β → Prop} (hp : ∀ b, Monotone fun a => p a b) :
    Monotone fun a => { b | p a b } := fun _ _ h b => hp b h

Monotonicity of Set Comprehension with Respect to a Preorder

Informal description

Let $\alpha$ be a preorder and $\beta$ be any type. Given a predicate $p : \alpha \to \beta \to \text{Prop}$ such that for every $b \in \beta$, the function $a \mapsto p(a, b)$ is monotone with respect to the preorder on $\alpha$, then the function $a \mapsto \{b \mid p(a, b)\}$ is also monotone.

Set.antitone_setOf theorem

[Preorder α] {p : α → β → Prop} (hp : ∀ b, Antitone fun a => p a b) : Antitone fun a => {b | p a b}

Full source

theorem antitone_setOf [Preorder α] {p : α → β → Prop} (hp : ∀ b, Antitone fun a => p a b) :
    Antitone fun a => { b | p a b } := fun _ _ h b => hp b h

Antitonicity of Set Comprehension with Antitone Predicate

Informal description

Let $\alpha$ be a preorder and $\beta$ be any type. Given a predicate $p : \alpha \to \beta \to \text{Prop}$ such that for every $b \in \beta$, the function $a \mapsto p(a, b)$ is antitone (i.e., decreasing with respect to the preorder on $\alpha$), then the function $a \mapsto \{b \mid p(a, b)\}$ is also antitone.

Set.antitone_bforall theorem

{P : α → Prop} : Antitone fun s : Set α => ∀ x ∈ s, P x

Full source

/-- Quantifying over a set is antitone in the set -/
theorem antitone_bforall {P : α → Prop} : Antitone fun s : Set α => ∀ x ∈ s, P x :=
  fun _ _ hst h x hx => h x <| hst hx

Antitonicity of Universal Quantification over Sets

Informal description

For any predicate $P$ on a type $\alpha$, the function that maps a set $s \subseteq \alpha$ to the proposition "$\forall x \in s, P(x)$" is antitone. That is, if $s \subseteq t$, then $(\forall x \in t, P(x))$ implies $(\forall x \in s, P(x))$.