MonovaryOn.symm
theorem MonovaryOn.symm :
∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β}
{s : Set ι}, MonovaryOn f g s → MonovaryOn g f s
The theorem `MonovaryOn.symm` states that for any types `ι`, `α`, and `β`, given a preorder on `α` and a linear order on `β`, for any two functions `f : ι → α` and `g : ι → β`, and a set `s` of type `ι`, if `f` monovaries with `g` on `s` then `g` also monovaries with `f` on `s`. In other words, if for all `i, j` in `s`, `g(i) < g(j)` implies `f(i) ≤ f(j)`, then it must also be the case that `f(i) < f(j)` implies `g(i) ≤ g(j)`.
More concisely: If a function `f` monovaries with respect to a function `g` on a set `s` in a preorder and a linear order, then `g` monovaries with respect to `f` on `s`.
|
Monovary.symm
theorem Monovary.symm :
∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β},
Monovary f g → Monovary g f
The theorem `Monovary.symm` states that for any types ι, α, β where α has a preordered structure and β has a linear ordered structure, and for any functions f: ι → α and g: ι → β, if f monovaries with g (meaning that whenever g(i) is less than g(j), f(i) is less than or equal to f(j)), then g also monovaries with f. In other words, if the values of g increase strictly then the values of f do not decrease, and conversely if the values of f do not decrease then the values of g increase strictly.
More concisely: If function `f: ι → α` monovaries with `g: ι → β`, where `α` has a preorder and `β` has a linear order, then `g` monovaries with `f`. (That is, if `g(i) < g(j)` implies `f(i) ≤ f(j)`, then `f(i) ≤ f(j)` implies `g(i) < g(j)`.)
|
monovaryOn_toDual_right
theorem monovaryOn_toDual_right :
∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι}, MonovaryOn f (⇑OrderDual.toDual ∘ g) s ↔ AntivaryOn f g s
The theorem `monovaryOn_toDual_right` establishes a relationship between two concepts of monotonicity, monovariation and antivariation, on a given set. Specifically, it says that for all preorders `α` and `β`, and for all functions `f : ι → α` and `g : ι → β`, and for any set `s` of type `ι`, the function `f` monovaries with the function `g`, where `g` is mapped to its dual order, on the set `s` if and only if `f` antivaries with `g` on `s`. In simpler terms, if increasing values of `g` (in its dual order) lead to non-decreasing values of `f`, then this is the same as saying that increasing values of `g` in its original order lead to non-increasing values of `f`.
More concisely: For all preorders α and β, functions f : ι -> α and g : ι -> β, and sets s of type ι, the function f monovaries with the dual of g on s if and only if f antivaries with g on s.
|
Antivary.antivaryOn
theorem Antivary.antivaryOn :
∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
Antivary f g → ∀ (s : Set ι), AntivaryOn f g s
The theorem `Antivary.antivaryOn` states that for any types `ι`, `α`, and `β` with preorders on `α` and `β`, and for any functions `f: ι → α` and `g: ι → β`, if `f` antivaries with `g`, then for any set `s` of type `ι`, `f` also antivaries with `g` on the set `s`. In other words, if the function `g` increases between any two elements, then the function `f` decreases (or stays the same) between those elements, not only over the whole domain but also when restricted to any subset of the domain.
More concisely: If functions `f: ι → α` and `g: ι → β` have the property that `f(x) ≤ f(y)` whenever `g(x) < g(y)` for all `x, y ∈ ι`, then `f` antivaries with `g` on any subset of `ι`.
|
Monovary.monovaryOn
theorem Monovary.monovaryOn :
∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
Monovary f g → ∀ (s : Set ι), MonovaryOn f g s
The theorem `Monovary.monovaryOn` states that for any types `ι`, `α`, and `β`, where `α` and `β` have a preorder relationship, any functions `f : ι → α` and `g : ι → β` that monovary, and any set `s` of type `ι`, `f` and `g` also monovary on `s`. In other words, if `f` and `g` satisfy the property that for all indices `i` and `j`, `g i < g j` implies `f i ≤ f j`, then this property also holds for all `i` and `j` that belong to the set `s`.
More concisely: If `f : ι → α` and `g : ι → β` are monovarying functions with `α` and `β` having a preorder relationship, and `g` is monotone on `ι`, then `f` and `g` are monovarying on any subset `s` of `ι`.
|
AntivaryOn.dual_right
theorem AntivaryOn.dual_right :
∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι}, AntivaryOn f g s → MonovaryOn f (⇑OrderDual.toDual ∘ g) s
The theorem `AntivaryOn.dual_right` states that for any types `ι`, `α`, and `β` with preorders on `α` and `β`, and any functions `f : ι → α`, `g : ι → β`, and a set `s : Set ι`, if `f` antivaries with `g` on `s`, then `f` monovaries with the dual order of `g` on `s`. In other words, if for all `i, j` in `s`, `g i < g j` implies `f j ≤ f i`, then applying the identity function to the dual order of `g`, for all `i, j` in `s`, `g i < g j` would imply `f i ≤ f j`. This theorem essentially establishes a connection between the behaviors of a function under the original and dual orders.
More concisely: If a function `f` antivaries with another function `g` on a set `s`, then `f` monovaries with the dual order of `g` on `s`.
|
Mathlib.Order.Monotone.Monovary._auxLemma.4
theorem Mathlib.Order.Monotone.Monovary._auxLemma.4 :
∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
AntivaryOn f g Set.univ = Antivary f g
This theorem states that for any given types `ι`, `α`, and `β`, with `α` and `β` being preordered, and any functions `f : ι → α` and `g : ι → β`, the property of `f` antivarying with `g` on the universal set (i.e., for all elements of `ι`) is equivalent to `f` antivarying with `g` without restriction to a specific set. In other words, if for every pair of elements `i` and `j` from `ι`, whenever `g(i)` is less than `g(j)`, `f(j)` is less than or equal to `f(i)`, this will hold true regardless of whether we consider all elements of `ι` (the case of `Antivary`) or restrict ourselves to a subset (the case of `AntivaryOn` with the universal set).
More concisely: For any preordered types `ι`, `α`, and `β`, and functions `f : ι → α` and `g : ι → β`, the condition that `f(i) ≤ f(j)` whenever `g(i) < g(j)` for all `i, j ∈ ι` is equivalent to `f` antivarying with `g` over `ι`, i.e., `Antivary f g ι`, and thus holds without restriction to any subset of `ι`.
|
Antivary.symm
theorem Antivary.symm :
∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β},
Antivary f g → Antivary g f
This theorem states that for any types `ι`, `α`, `β` where `α` and `β` have a preorder and `β` has a linear order, if a function `f` from `ι` to `α` antivaries with a function `g` from `ι` to `β` (meaning that whenever `g(i)` is less than `g(j)`, `f(j)` is less than or equal to `f(i)`), then it must be the case that `g` antivaries with `f` as well. In other words, if `f(i)` is less than `f(j)`, then `g(j)` must be less than or equal to `g(i)`. This theorem essentially states that the antivariation relationship between two functions is symmetric.
More concisely: If `f: ι → α` antivaries with `g: ι → β`, where `α` and `β` have a preorder and `β` has a linear order, then `g` antivaries with `f`. That is, `f(i) ≤ f(j)` implies `g(j) ≤ g(i)`.
|
AntivaryOn.symm
theorem AntivaryOn.symm :
∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β}
{s : Set ι}, AntivaryOn f g s → AntivaryOn g f s
The theorem `AntivaryOn.symm` states that for any types `ι`, `α`, and `β`, with `α` and `β` equipped with a Preorder structure and `β` additionally having a LinearOrder structure, any two functions `f: ι → α` and `g: ι → β`, and any set `s` of type `ι`, if `f` antivaries with `g` on `s`, then `g` also antivaries with `f` on `s`. Here, a function `f` is said to antivary with a function `g` on a set `s` if for all elements `i` and `j` in `s`, a smaller value of `g` (i.e., `g i < g j`) implies a larger or equal value of `f` (i.e., `f j ≤ f i`).
More concisely: If functions $f: ι → α$ and $g: ι → β$ have $f(j) ≤ f(i)$ for all $i, j \in s$ whenever $g(i) < g(j)$, then $g(j) ≤ g(i)$ implies $f(i) ≤ f(j)$ for all $i, j \in s$.
|
Mathlib.Order.Monotone.Monovary._auxLemma.3
theorem Mathlib.Order.Monotone.Monovary._auxLemma.3 :
∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
MonovaryOn f g Set.univ = Monovary f g
This theorem states that for any types `ι`, `α`, and `β`, and given preordered types `α` and `β`, the function `f` from `ι` to `α` and function `g` from `ι` to `β`, the property of `f` monovarying with `g` on the universal set (i.e., for all elements in `ι`) is equivalent to `f` monovarying with `g` in general. In other words, `f` monovaries with `g` if and only if `f` monovaries with `g` for all values in the type `ι`. Here, a function `f` is said to monovary with a function `g` if whenever `g i` is less than `g j`, `f i` is less than or equal to `f j`.
More concisely: For functions `f:` ι -> α and `g:` ι -> β between preordered types, `f` monovaries with `g` if and only if `f` monovaries with `g` on the universal set.
|