Mathlib.Data.Set.Monotone

MonotoneOn.congr theorem

(h₁ : MonotoneOn f₁ s) (h : s.EqOn f₁ f₂) : MonotoneOn f₂ s

Full source

theorem _root_.MonotoneOn.congr (h₁ : MonotoneOn f₁ s) (h : s.EqOn f₁ f₂) : MonotoneOn f₂ s := by
  intro a ha b hb hab
  rw [← h ha, ← h hb]
  exact h₁ ha hb hab

Monotonicity is preserved under function equality on a set

Informal description

Let $f₁$ and $f₂$ be functions defined on a set $s$. If $f₁$ is monotone on $s$ and $f₁$ coincides with $f₂$ on $s$ (i.e., $f₁(x) = f₂(x)$ for all $x \in s$), then $f₂$ is also monotone on $s$.

AntitoneOn.congr theorem

(h₁ : AntitoneOn f₁ s) (h : s.EqOn f₁ f₂) : AntitoneOn f₂ s

Full source

theorem _root_.AntitoneOn.congr (h₁ : AntitoneOn f₁ s) (h : s.EqOn f₁ f₂) : AntitoneOn f₂ s :=
  h₁.dual_right.congr h

Decreasing Property is Preserved Under Function Equality on a Set

Informal description

Let $f_1$ and $f_2$ be functions defined on a set $s$. If $f_1$ is decreasing on $s$ and $f_1(x) = f_2(x)$ for all $x \in s$, then $f_2$ is also decreasing on $s$.

StrictMonoOn.congr theorem

(h₁ : StrictMonoOn f₁ s) (h : s.EqOn f₁ f₂) : StrictMonoOn f₂ s

Full source

theorem _root_.StrictMonoOn.congr (h₁ : StrictMonoOn f₁ s) (h : s.EqOn f₁ f₂) :
    StrictMonoOn f₂ s := by
  intro a ha b hb hab
  rw [← h ha, ← h hb]
  exact h₁ ha hb hab

Strict Monotonicity is Preserved Under Function Equality on a Set

Informal description

Let $f₁$ and $f₂$ be functions defined on a set $s$. If $f₁$ is strictly increasing on $s$ and $f₁$ and $f₂$ are equal on $s$, then $f₂$ is also strictly increasing on $s$.

StrictAntiOn.congr theorem

(h₁ : StrictAntiOn f₁ s) (h : s.EqOn f₁ f₂) : StrictAntiOn f₂ s

Full source

theorem _root_.StrictAntiOn.congr (h₁ : StrictAntiOn f₁ s) (h : s.EqOn f₁ f₂) : StrictAntiOn f₂ s :=
  h₁.dual_right.congr h

Strict Decreasing Property is Preserved Under Function Equality on a Set

Informal description

Let $f_1$ and $f_2$ be functions defined on a set $s$. If $f_1$ is strictly decreasing on $s$ and $f_1(x) = f_2(x)$ for all $x \in s$, then $f_2$ is also strictly decreasing on $s$.

Set.EqOn.congr_monotoneOn theorem

(h : s.EqOn f₁ f₂) : MonotoneOn f₁ s ↔ MonotoneOn f₂ s

Full source

theorem EqOn.congr_monotoneOn (h : s.EqOn f₁ f₂) : MonotoneOnMonotoneOn f₁ s ↔ MonotoneOn f₂ s :=
  ⟨fun h₁ => h₁.congr h, fun h₂ => h₂.congr h.symm⟩

Monotonicity Equivalence Under Function Equality on a Set

Informal description

Let $f_1$ and $f_2$ be functions defined on a set $s$. If $f_1$ and $f_2$ are equal on $s$ (i.e., $f_1(x) = f_2(x)$ for all $x \in s$), then $f_1$ is monotone on $s$ if and only if $f_2$ is monotone on $s$.

Set.EqOn.congr_antitoneOn theorem

(h : s.EqOn f₁ f₂) : AntitoneOn f₁ s ↔ AntitoneOn f₂ s

Full source

theorem EqOn.congr_antitoneOn (h : s.EqOn f₁ f₂) : AntitoneOnAntitoneOn f₁ s ↔ AntitoneOn f₂ s :=
  ⟨fun h₁ => h₁.congr h, fun h₂ => h₂.congr h.symm⟩

Equivalence of Decreasing Property Under Function Equality on a Set

Informal description

Let $f_1$ and $f_2$ be functions defined on a set $s$. If $f_1$ and $f_2$ are equal on $s$ (i.e., $f_1(x) = f_2(x)$ for all $x \in s$), then $f_1$ is decreasing on $s$ if and only if $f_2$ is decreasing on $s$.

Set.EqOn.congr_strictMonoOn theorem

(h : s.EqOn f₁ f₂) : StrictMonoOn f₁ s ↔ StrictMonoOn f₂ s

Full source

theorem EqOn.congr_strictMonoOn (h : s.EqOn f₁ f₂) : StrictMonoOnStrictMonoOn f₁ s ↔ StrictMonoOn f₂ s :=
  ⟨fun h₁ => h₁.congr h, fun h₂ => h₂.congr h.symm⟩

Equivalence of Strict Monotonicity Under Function Equality on a Set

Informal description

Let $f_1$ and $f_2$ be functions defined on a set $s$. If $f_1(x) = f_2(x)$ for all $x \in s$, then $f_1$ is strictly increasing on $s$ if and only if $f_2$ is strictly increasing on $s$.

Set.EqOn.congr_strictAntiOn theorem

(h : s.EqOn f₁ f₂) : StrictAntiOn f₁ s ↔ StrictAntiOn f₂ s

Full source

theorem EqOn.congr_strictAntiOn (h : s.EqOn f₁ f₂) : StrictAntiOnStrictAntiOn f₁ s ↔ StrictAntiOn f₂ s :=
  ⟨fun h₁ => h₁.congr h, fun h₂ => h₂.congr h.symm⟩

Equivalence of Strict Decreasing Property Under Function Equality on a Set

Informal description

Let $f_1$ and $f_2$ be functions defined on a set $s$. If $f_1(x) = f_2(x)$ for all $x \in s$, then $f_1$ is strictly decreasing on $s$ if and only if $f_2$ is strictly decreasing on $s$.

MonotoneOn.mono theorem

(h : MonotoneOn f s) (h' : s₂ ⊆ s) : MonotoneOn f s₂

Full source

theorem _root_.MonotoneOn.mono (h : MonotoneOn f s) (h' : s₂ ⊆ s) : MonotoneOn f s₂ :=
  fun _ hx _ hy => h (h' hx) (h' hy)

Monotonicity is Preserved Under Subset Restriction

Informal description

Let $f$ be a function that is monotone on a set $s$. If $s_2$ is a subset of $s$, then $f$ is also monotone on $s_2$.

AntitoneOn.mono theorem

(h : AntitoneOn f s) (h' : s₂ ⊆ s) : AntitoneOn f s₂

Full source

theorem _root_.AntitoneOn.mono (h : AntitoneOn f s) (h' : s₂ ⊆ s) : AntitoneOn f s₂ :=
  fun _ hx _ hy => h (h' hx) (h' hy)

Restriction of Antitone Function to Subset Preserves Antitonicity

Informal description

If a function $f$ is antitone on a set $s$ (i.e., for any $x, y \in s$, $x \leq y$ implies $f(x) \geq f(y)$), and $s_2$ is a subset of $s$, then $f$ is also antitone on $s_2$.

StrictMonoOn.mono theorem

(h : StrictMonoOn f s) (h' : s₂ ⊆ s) : StrictMonoOn f s₂

Full source

theorem _root_.StrictMonoOn.mono (h : StrictMonoOn f s) (h' : s₂ ⊆ s) : StrictMonoOn f s₂ :=
  fun _ hx _ hy => h (h' hx) (h' hy)

Strict Monotonicity is Preserved Under Subset Restriction

Informal description

If a function $f$ is strictly increasing on a set $s$, then it is also strictly increasing on any subset $s_2 \subseteq s$.

StrictAntiOn.mono theorem

(h : StrictAntiOn f s) (h' : s₂ ⊆ s) : StrictAntiOn f s₂

Full source

theorem _root_.StrictAntiOn.mono (h : StrictAntiOn f s) (h' : s₂ ⊆ s) : StrictAntiOn f s₂ :=
  fun _ hx _ hy => h (h' hx) (h' hy)

Strict Antitonicity is Preserved Under Subset Restriction

Informal description

Let $f$ be a function and $s$ a set. If $f$ is strictly antitone on $s$ (i.e., for any $x, y \in s$, $x < y$ implies $f(x) > f(y)$), and $s_2$ is a subset of $s$, then $f$ is strictly antitone on $s_2$.

MonotoneOn.monotone theorem

(h : MonotoneOn f s) : Monotone (f ∘ Subtype.val : s → β)

Full source

protected theorem _root_.MonotoneOn.monotone (h : MonotoneOn f s) :
    Monotone (f ∘ Subtype.val : s → β) :=
  fun x y hle => h x.coe_prop y.coe_prop hle

Monotonicity of a Function Restricted to a Monotone Set

Informal description

If a function $f$ is monotone on a set $s$, then the restriction of $f$ to $s$ (viewed as a function from $s$ to $\beta$) is monotone.

AntitoneOn.monotone theorem

(h : AntitoneOn f s) : Antitone (f ∘ Subtype.val : s → β)

Full source

protected theorem _root_.AntitoneOn.monotone (h : AntitoneOn f s) :
    Antitone (f ∘ Subtype.val : s → β) :=
  fun x y hle => h x.coe_prop y.coe_prop hle

Antitone Restriction of an Antitone Function

Informal description

If a function $f$ is antitone on a set $s$ (i.e., for any $x, y \in s$, $x \leq y$ implies $f(x) \geq f(y)$), then the restriction of $f$ to $s$ (viewed as a function from $s$ to $\beta$) is antitone.

StrictMonoOn.strictMono theorem

(h : StrictMonoOn f s) : StrictMono (f ∘ Subtype.val : s → β)

Full source

protected theorem _root_.StrictMonoOn.strictMono (h : StrictMonoOn f s) :
    StrictMono (f ∘ Subtype.val : s → β) :=
  fun x y hlt => h x.coe_prop y.coe_prop hlt

Strict Monotonicity of Restricted Function from Strict Monotonicity on Set

Informal description

If a function $f$ is strictly monotone on a set $s$, then the restriction of $f$ to $s$ (viewed as a function on the subtype $s$) is strictly monotone.

StrictAntiOn.strictAnti theorem

(h : StrictAntiOn f s) : StrictAnti (f ∘ Subtype.val : s → β)

Full source

protected theorem _root_.StrictAntiOn.strictAnti (h : StrictAntiOn f s) :
    StrictAnti (f ∘ Subtype.val : s → β) :=
  fun x y hlt => h x.coe_prop y.coe_prop hlt

Strictly Antitone Restriction of a Strictly Antitone Function

Informal description

If a function $f$ is strictly antitone on a set $s \subseteq \alpha$, then the restriction of $f$ to $s$ (viewed as a function from $s$ to $\beta$) is strictly antitone. That is, for any $x, y \in s$, if $x < y$ then $f(y) < f(x)$.

Set.MonotoneOn_insert_iff theorem

 {a : α} : MonotoneOn f (insert a s) ↔ (∀ b ∈ s, b ≤ a → f b ≤ f a) ∧ (∀ b ∈ s, a ≤ b → f a ≤ f b) ∧ MonotoneOn f s

Full source

lemma MonotoneOn_insert_iff {a : α} :
    MonotoneOnMonotoneOn f (insert a s) ↔
      (∀ b ∈ s, b ≤ a → f b ≤ f a) ∧ (∀ b ∈ s, a ≤ b → f a ≤ f b) ∧ MonotoneOn f s := by
  simp [MonotoneOn, forall_and]

Characterization of Monotonicity on Inserted Set

Informal description

Let $f$ be a function from a set $\alpha$ to a partially ordered set, and let $s \subseteq \alpha$ be a subset. For any element $a \in \alpha$, the function $f$ is monotone on the set $\{a\} \cup s$ if and only if the following three conditions hold: 1. For all $b \in s$, if $b \leq a$ then $f(b) \leq f(a)$, 2. For all $b \in s$, if $a \leq b$ then $f(a) \leq f(b)$, 3. $f$ is monotone on $s$.

Set.AntitoneOn_insert_iff theorem

 {a : α} : AntitoneOn f (insert a s) ↔ (∀ b ∈ s, b ≤ a → f a ≤ f b) ∧ (∀ b ∈ s, a ≤ b → f b ≤ f a) ∧ AntitoneOn f s

Full source

lemma AntitoneOn_insert_iff {a : α} :
    AntitoneOnAntitoneOn f (insert a s) ↔
      (∀ b ∈ s, b ≤ a → f a ≤ f b) ∧ (∀ b ∈ s, a ≤ b → f b ≤ f a) ∧ AntitoneOn f s :=
  @MonotoneOn_insert_iff α βᵒᵈ _ _ _ _ _

Characterization of Antitonicity on Inserted Set

Informal description

Let $f$ be a function from a set $\alpha$ to a partially ordered set, and let $s \subseteq \alpha$ be a subset. For any element $a \in \alpha$, the function $f$ is antitone on the set $\{a\} \cup s$ if and only if the following three conditions hold: 1. For all $b \in s$, if $b \leq a$ then $f(a) \leq f(b)$, 2. For all $b \in s$, if $a \leq b$ then $f(b) \leq f(a)$, 3. $f$ is antitone on $s$.

Monotone.restrict theorem

(h : Monotone f) (s : Set α) : Monotone (s.restrict f)

Full source

protected theorem restrict (h : Monotone f) (s : Set α) : Monotone (s.restrict f) := fun _ _ hxy =>
  h hxy

Monotonicity is Preserved under Restriction

Informal description

If $f : \alpha \to \beta$ is a monotone function and $s$ is a subset of $\alpha$, then the restriction of $f$ to $s$ is also monotone.

Monotone.codRestrict theorem

(h : Monotone f) {s : Set β} (hs : ∀ x, f x ∈ s) : Monotone (s.codRestrict f hs)

Full source

protected theorem codRestrict (h : Monotone f) {s : Set β} (hs : ∀ x, f x ∈ s) :
    Monotone (s.codRestrict f hs) :=
  h

Monotonicity is preserved under codomain restriction

Informal description

Let $f : \alpha \to \beta$ be a monotone function between preorders, and let $s \subseteq \beta$ be a subset such that $f(x) \in s$ for all $x \in \alpha$. Then the codomain-restricted function $f \restriction^s : \alpha \to s$ (mapping $x$ to $\langle f(x), hs(x) \rangle$) is also monotone.

Monotone.rangeFactorization theorem

(h : Monotone f) : Monotone (Set.rangeFactorization f)

Full source

protected theorem rangeFactorization (h : Monotone f) : Monotone (Set.rangeFactorization f) :=
  h

Monotonicity is preserved under range factorization

Informal description

If a function $f : \alpha \to \beta$ is monotone, then its range factorization (the function obtained by restricting the codomain to the range of $f$) is also monotone.

StrictMonoOn.injOn theorem

[LinearOrder α] [Preorder β] {f : α → β} {s : Set α} (H : StrictMonoOn f s) : s.InjOn f

Full source

theorem StrictMonoOn.injOn [LinearOrder α] [Preorder β] {f : α → β} {s : Set α}
    (H : StrictMonoOn f s) : s.InjOn f := fun x hx y hy hxy =>
  show Ordering.eq.Compares x y from (H.compares hx hy).1 hxy

Strictly Increasing Functions on Linearly Ordered Sets are Injective

Informal description

Let $\alpha$ be a linearly ordered set and $\beta$ a preordered set. If a function $f : \alpha \to \beta$ is strictly increasing on a subset $s \subseteq \alpha$, then $f$ is injective on $s$.

StrictAntiOn.injOn theorem

[LinearOrder α] [Preorder β] {f : α → β} {s : Set α} (H : StrictAntiOn f s) : s.InjOn f

Full source

theorem StrictAntiOn.injOn [LinearOrder α] [Preorder β] {f : α → β} {s : Set α}
    (H : StrictAntiOn f s) : s.InjOn f :=
  @StrictMonoOn.injOn α βᵒᵈ _ _ f s H

Strictly Decreasing Functions on Linearly Ordered Sets are Injective

Informal description

Let $\alpha$ be a linearly ordered set and $\beta$ a preordered set. If a function $f : \alpha \to \beta$ is strictly decreasing on a subset $s \subseteq \alpha$, then $f$ is injective on $s$.

StrictMonoOn.comp theorem

 [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : StrictMonoOn g t)
  (hf : StrictMonoOn f s) (hs : Set.MapsTo f s t) : StrictMonoOn (g ∘ f) s

Full source

theorem StrictMonoOn.comp [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α}
    {t : Set β} (hg : StrictMonoOn g t) (hf : StrictMonoOn f s) (hs : Set.MapsTo f s t) :
    StrictMonoOn (g ∘ f) s := fun _x hx _y hy hxy => hg (hs hx) (hs hy) <| hf hx hy hxy

Composition of Strictly Increasing Functions is Strictly Increasing

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be preordered sets, and let $f : \alpha \to \beta$ and $g : \beta \to \gamma$ be functions. Given subsets $s \subseteq \alpha$ and $t \subseteq \beta$ such that $f$ maps $s$ into $t$, if $g$ is strictly increasing on $t$ and $f$ is strictly increasing on $s$, then the composition $g \circ f$ is strictly increasing on $s$.

StrictMonoOn.comp_strictAntiOn theorem

 [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : StrictMonoOn g t)
  (hf : StrictAntiOn f s) (hs : Set.MapsTo f s t) : StrictAntiOn (g ∘ f) s

Full source

theorem StrictMonoOn.comp_strictAntiOn [Preorder α] [Preorder β] [Preorder γ] {g : β → γ}
    {f : α → β} {s : Set α} {t : Set β} (hg : StrictMonoOn g t) (hf : StrictAntiOn f s)
    (hs : Set.MapsTo f s t) : StrictAntiOn (g ∘ f) s := fun _x hx _y hy hxy =>
  hg (hs hy) (hs hx) <| hf hx hy hxy

Composition of Strictly Increasing and Strictly Decreasing Functions is Strictly Decreasing

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be types equipped with preorders, and let $f : \alpha \to \beta$ and $g : \beta \to \gamma$ be functions. Given subsets $s \subseteq \alpha$ and $t \subseteq \beta$ such that $f$ maps $s$ into $t$, if $g$ is strictly increasing on $t$ and $f$ is strictly decreasing on $s$, then the composition $g \circ f$ is strictly decreasing on $s$.

StrictAntiOn.comp theorem

 [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : StrictAntiOn g t)
  (hf : StrictAntiOn f s) (hs : Set.MapsTo f s t) : StrictMonoOn (g ∘ f) s

Full source

theorem StrictAntiOn.comp [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α}
    {t : Set β} (hg : StrictAntiOn g t) (hf : StrictAntiOn f s) (hs : Set.MapsTo f s t) :
    StrictMonoOn (g ∘ f) s := fun _x hx _y hy hxy => hg (hs hy) (hs hx) <| hf hx hy hxy

Composition of Strictly Antitone Functions is Strictly Monotone

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be preordered sets, and let $f : \alpha \to \beta$ and $g : \beta \to \gamma$ be functions. Given subsets $s \subseteq \alpha$ and $t \subseteq \beta$ such that $f$ maps $s$ into $t$, if $g$ is strictly antitone on $t$ and $f$ is strictly antitone on $s$, then the composition $g \circ f$ is strictly monotone on $s$.

StrictAntiOn.comp_strictMonoOn theorem

 [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : StrictAntiOn g t)
  (hf : StrictMonoOn f s) (hs : Set.MapsTo f s t) : StrictAntiOn (g ∘ f) s

Full source

theorem StrictAntiOn.comp_strictMonoOn [Preorder α] [Preorder β] [Preorder γ] {g : β → γ}
    {f : α → β} {s : Set α} {t : Set β} (hg : StrictAntiOn g t) (hf : StrictMonoOn f s)
    (hs : Set.MapsTo f s t) : StrictAntiOn (g ∘ f) s := fun _x hx _y hy hxy =>
  hg (hs hx) (hs hy) <| hf hx hy hxy

Composition of Strictly Antitone and Strictly Monotone Functions is Strictly Antitone

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be preordered sets. Given functions $g : \beta \to \gamma$ and $f : \alpha \to \beta$, and subsets $s \subseteq \alpha$ and $t \subseteq \beta$, if: 1. $g$ is strictly antitone on $t$, 2. $f$ is strictly monotone on $s$, and 3. $f$ maps $s$ into $t$, then the composition $g \circ f$ is strictly antitone on $s$.

strictMono_restrict theorem

[Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictMono (s.restrict f) ↔ StrictMonoOn f s

Full source

@[simp]
theorem strictMono_restrict [Preorder α] [Preorder β] {f : α → β} {s : Set α} :
    StrictMonoStrictMono (s.restrict f) ↔ StrictMonoOn f s := by simp [Set.restrict, StrictMono, StrictMonoOn]

Strict Monotonicity of Function Restriction

Informal description

Let $α$ and $β$ be preorders, $f : α → β$ a function, and $s$ a subset of $α$. The restriction of $f$ to $s$ is strictly monotone if and only if $f$ is strictly monotone on $s$.

StrictMono.codRestrict theorem

 [Preorder α] [Preorder β] {f : α → β} (hf : StrictMono f) {s : Set β} (hs : ∀ x, f x ∈ s) :
  StrictMono (Set.codRestrict f s hs)

Full source

theorem StrictMono.codRestrict [Preorder α] [Preorder β] {f : α → β} (hf : StrictMono f)
    {s : Set β} (hs : ∀ x, f x ∈ s) : StrictMono (Set.codRestrict f s hs) :=
  hf

Strict Monotonicity is Preserved Under Codomain Restriction

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $f : \alpha \to \beta$ be a strictly monotone function. For any subset $s \subseteq \beta$ such that $f(x) \in s$ for all $x \in \alpha$, the codomain restriction of $f$ to $s$ remains strictly monotone.

strictMonoOn_insert_iff theorem

 [Preorder α] [Preorder β] {f : α → β} {s : Set α} {a : α} :
  StrictMonoOn f (insert a s) ↔ (∀ b ∈ s, b < a → f b < f a) ∧ (∀ b ∈ s, a < b → f a < f b) ∧ StrictMonoOn f s

Full source

lemma strictMonoOn_insert_iff [Preorder α] [Preorder β] {f : α → β} {s : Set α} {a : α} :
    StrictMonoOnStrictMonoOn f (insert a s) ↔
       (∀ b ∈ s, b < a → f b < f a) ∧ (∀ b ∈ s, a < b → f a < f b) ∧ StrictMonoOn f s := by
  simp [StrictMonoOn, forall_and]

Characterization of Strict Monotonicity on Extended Set via Insertion

Informal description

Let $\alpha$ and $\beta$ be preordered sets, $f : \alpha \to \beta$ a function, $s \subseteq \alpha$ a subset, and $a \in \alpha$ an element. Then $f$ is strictly monotone on $s \cup \{a\}$ if and only if the following three conditions hold: 1. For all $b \in s$, if $b < a$ then $f(b) < f(a)$, 2. For all $b \in s$, if $a < b$ then $f(a) < f(b)$, 3. $f$ is strictly monotone on $s$.

strictAntiOn_insert_iff theorem

 [Preorder α] [Preorder β] {f : α → β} {s : Set α} {a : α} :
  StrictAntiOn f (insert a s) ↔ (∀ b ∈ s, b < a → f a < f b) ∧ (∀ b ∈ s, a < b → f b < f a) ∧ StrictAntiOn f s

Full source

lemma strictAntiOn_insert_iff [Preorder α] [Preorder β] {f : α → β} {s : Set α} {a : α} :
    StrictAntiOnStrictAntiOn f (insert a s) ↔
       (∀ b ∈ s, b < a → f a < f b) ∧ (∀ b ∈ s, a < b → f b < f a) ∧ StrictAntiOn f s :=
  @strictMonoOn_insert_iff α βᵒᵈ _ _ _ _ _

Characterization of Strict Antitonicity on Extended Set via Insertion

Informal description

Let $\alpha$ and $\beta$ be preordered sets, $f : \alpha \to \beta$ a function, $s \subseteq \alpha$ a subset, and $a \in \alpha$ an element. Then $f$ is strictly antitone on $s \cup \{a\}$ if and only if the following three conditions hold: 1. For all $b \in s$, if $b < a$ then $f(a) < f(b)$, 2. For all $b \in s$, if $a < b$ then $f(b) < f(a)$, 3. $f$ is strictly antitone on $s$.

Function.monotoneOn_of_rightInvOn_of_mapsTo theorem

 {α β : Type*} [PartialOrder α] [LinearOrder β] {φ : β → α} {ψ : α → β} {t : Set β} {s : Set α} (hφ : MonotoneOn φ t)
  (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) : MonotoneOn ψ s

Full source

theorem monotoneOn_of_rightInvOn_of_mapsTo {α β : Type*} [PartialOrder α] [LinearOrder β]
    {φ : β → α} {ψ : α → β} {t : Set β} {s : Set α} (hφ : MonotoneOn φ t)
    (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) : MonotoneOn ψ s := by
  rintro x xs y ys l
  rcases le_total (ψ x) (ψ y) with (ψxy|ψyx)
  · exact ψxy
  · have := hφ (ψts ys) (ψts xs) ψyx
    rw [φψs.eq ys, φψs.eq xs] at this
    induction le_antisymm l this
    exact le_refl _

Monotonicity of Right Inverse Function on Restricted Domain

Informal description

Let $\alpha$ be a partially ordered set and $\beta$ a linearly ordered set. Given functions $\phi : \beta \to \alpha$ and $\psi : \alpha \to \beta$, a subset $t \subseteq \beta$, and a subset $s \subseteq \alpha$, if: 1. $\phi$ is monotone on $t$, 2. $\psi$ is a right inverse of $\phi$ on $s$ (i.e., $\phi(\psi(x)) = x$ for all $x \in s$), 3. $\psi$ maps $s$ into $t$, then $\psi$ is monotone on $s$.

Function.antitoneOn_of_rightInvOn_of_mapsTo theorem

 [PartialOrder α] [LinearOrder β] {φ : β → α} {ψ : α → β} {t : Set β} {s : Set α} (hφ : AntitoneOn φ t)
  (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) : AntitoneOn ψ s

Full source

theorem antitoneOn_of_rightInvOn_of_mapsTo [PartialOrder α] [LinearOrder β]
    {φ : β → α} {ψ : α → β} {t : Set β} {s : Set α} (hφ : AntitoneOn φ t)
    (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) : AntitoneOn ψ s :=
  (monotoneOn_of_rightInvOn_of_mapsTo hφ.dual_left φψs ψts).dual_right

Antitonicity of Right Inverse Function on Restricted Domain

Informal description

Let $\alpha$ be a partially ordered set and $\beta$ a linearly ordered set. Given functions $\phi : \beta \to \alpha$ and $\psi : \alpha \to \beta$, a subset $t \subseteq \beta$, and a subset $s \subseteq \alpha$, if: 1. $\phi$ is antitone on $t$, 2. $\psi$ is a right inverse of $\phi$ on $s$ (i.e., $\phi(\psi(x)) = x$ for all $x \in s$), 3. $\psi$ maps $s$ into $t$, then $\psi$ is antitone on $s$.