Covariant.flip
theorem Covariant.flip :
∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop}, Covariant M N μ r → Covariant M N μ (flip r)
The theorem `Covariant.flip` states that for all types `M` and `N`, a function `μ : M → N → N`, and a relation `r` on `N`, if `μ` is covariant with respect to `r`, then `μ` is also covariant with respect to the flipped relation of `r`. Here, a function is called covariant with respect to a relation if applying the function to two elements does not change the relation between them. The flip of a relation is a new relation where the order of arguments is reversed. In other words, if `μ` preserves the relation `r` between two elements of `N`, then it also preserves the relation `r` when the order of these elements is reversed.
More concisely: If a function `μ : M → N → N` is covariant with respect to a relation `r` on `N`, then it is also covariant with respect to the flipped relation of `r`.
|
Antitone.covariant_of_const'
theorem Antitone.covariant_of_const' :
∀ {N : Type u_2} {α : Type u_3} [inst : Preorder α] [inst_1 : Preorder N] {f : N → α} {μ : N → N → N}
[inst_2 : CovariantClass N N (Function.swap μ) fun x x_1 => x ≤ x_1],
Antitone f → ∀ (m : N), Antitone fun x => f (μ x m)
The theorem `Antitone.covariant_of_const'` states that for any two types `N` and `α` that have a preorder relation, if there is a function `f` from `N` to `α` and a binary function `μ` on `N` that is covariant when its arguments are swapped and `f` is an antitone function (i.e., `f` is decreasing in the preorder sense), then for any element `m` of `N`, the function that takes `x` to `f(μ(x, m))` is also antitone. In other words, if `f` is decreasing and `μ` respects the order of its arguments when swapped, then the composition of `f` with `μ` in this specific manner also respects the order in a decreasing way.
More concisely: If `f` is an antitone function between preordered types `N` and `α`, and `μ` is a covariant function on `N`, then the function `x mapsto f(μ(x, m))` is also antitone for any `m` in `N`.
|
ContravariantClass.elim
theorem ContravariantClass.elim :
∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [self : ContravariantClass M N μ r],
Contravariant M N μ r
The theorem states that for any type `M`, type `N`, function `μ` from `M` and `N` to `N`, and a relation `r` on `N`, assuming we have a `ContravariantClass` instance for `M`, `N`, `μ` and `r`, then the contravariant property holds. This contravariant property is defined as follows: for every `m` in `M`, and for any elements `n₁, n₂` in `N`, if the relation `r` holds between the result of applying `m` to `n₁` and `n₂` (i.e., `r (μ m n₁) (μ m n₂)`), then the same relation `r` also holds between `n₁` and `n₂` directly, i.e., `r n₁ n₂`. This theorem essentially asserts that the `ContravariantClass` ensures this property.
More concisely: Given a relation `r` on a type `N`, a function `μ` from a type `M` to `N`, and assuming `M`, `N`, `μ`, and `r` have a `ContravariantClass` instance, if `r` holds between the application of `μ` to `m` in `M` and two elements `n₁, n₂` in `N`, then `r` holds between `n₁` and `n₂`.
|
Monotone.covariant_of_const
theorem Monotone.covariant_of_const :
∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {α : Type u_3} [inst : Preorder α] [inst_1 : Preorder N] {f : N → α}
[inst_2 : CovariantClass M N μ fun x x_1 => x ≤ x_1], Monotone f → ∀ (m : M), Monotone fun x => f (μ m x)
This theorem states that if we have a function `f` which is monotone from a preordered set `N` to another preordered set `α`, and we have a covariant operator `μ` (which is a binary function that preserves the order from `M` to `N`), then the composition of `f` with the partial application of `μ` to some element `m` from `M` is also a monotone function. In other words, for any `m`, if `f` is monotone then the function which maps `x` to `f(μ m x)` is monotone. This could be seen in a concrete example such as `∀ (m : ℕ), Monotone f → Monotone (fun n ↦ f (m + n))`, where natural numbers are added to `n` and the result is passed to the monotone function `f`.
More concisely: If `f` is a monotone function from a preordered set `N` to another preordered set `α`, and `μ` is a covariant operator from a preordered set `M` to `N`, then the function `x ↦ f(μ(m) x)` is monotone for any `m` in `M`.
|
contravariant_le_iff_contravariant_lt_and_eq
theorem contravariant_le_iff_contravariant_lt_and_eq :
∀ (M : Type u_1) (N : Type u_2) (μ : M → N → N) [inst : PartialOrder N],
(Contravariant M N μ fun x x_1 => x ≤ x_1) ↔
(Contravariant M N μ fun x x_1 => x < x_1) ∧ Contravariant M N μ fun x x_1 => x = x_1
The theorem `contravariant_le_iff_contravariant_lt_and_eq` states that for any two types `M` and `N`, and a function `μ` from `M` and `N` to `N`, under a partial order on `N`, the contravariant property with respect to the "less than or equal to" relation is equivalent to the contravariant property both with respect to the "less than" relation and the "equal to" relation. This means that if the action of any element in `M` preserves the "less than or equal to" ordering of elements in `N`, then it also preserves the "less than" and "equal to" orderings, and vice versa.
More concisely: For any type `M`, type `N`, and function `μ` from `M` to `N` under a partial order on `N`, the contravariant property with respect to the relation "less than or equal to" on `N` is equivalent to the simultaneous contravariant properties with respect to both "less than" and "equal to" relations on `N`.
|
Contravariant.flip
theorem Contravariant.flip :
∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop},
Contravariant M N μ r → Contravariant M N μ (flip r)
The theorem `Contravariant.flip` states that for any types `M` and `N`, a function `μ` from `M` and `N` to `N`, and a relation `r` on `N`, if `μ` is contravariant with respect to `r`, then it is also contravariant with respect to the flipped version of `r`. In other words, if for all `m` in `M` and `n₁`, `n₂` in `N`, `r` applied to `μ(m, n₁)` and `μ(m, n₂)` implies `r(n₁, n₂)`, then the same is true if we swap the arguments of `r` in the implication.
More concisely: If a function between types is contravariant with respect to a relation, then it is also contravariant with respect to the flipped version of that relation.
|
rel_iff_cov
theorem rel_iff_cov :
∀ (M : Type u_1) (N : Type u_2) (μ : M → N → N) (r : N → N → Prop) [inst : CovariantClass M N μ r]
[inst : ContravariantClass M N μ r] (m : M) {a b : N}, r (μ m a) (μ m b) ↔ r a b
This theorem, `rel_iff_cov`, states that for any types `M` and `N`, a binary operation `μ` from `M` and `N` to `N`, and a binary relation `r` on `N`, if `M` and `N` form a covariant class under `μ` and `r`, and also form a contravariant class under `μ` and `r`, then for any element `m` of `M` and any elements `a` and `b` of `N`, the relation `r` holds between `μ(m, a)` and `μ(m, b)` if and only if the same relation `r` holds between `a` and `b`. In other words, under these conditions, applying the operation `μ` with `m` to `a` and `b` preserves the relation `r`.
More concisely: If types `M` and `N`, binary operation `μ`, and binary relation `r` satisfy `M` and `N` being covariant and contravariant classes under `μ` and `r`, then `r(μ(m, a), μ(m, b)) <-> r(a, b)` for all `m ∈ M` and `a, b ∈ N`.
|
covariant_lt_iff_contravariant_le
theorem covariant_lt_iff_contravariant_le :
∀ (M : Type u_1) (N : Type u_2) (μ : M → N → N) [inst : LinearOrder N],
(Covariant M N μ fun x x_1 => x < x_1) ↔ Contravariant M N μ fun x x_1 => x ≤ x_1
The theorem `covariant_lt_iff_contravariant_le` asserts that for any two types `M` and `N`, and a function `μ` mapping from `M` and `N` to `N`, given a linear order on `N`, the property that `μ` is covariant with respect to the "less than" relation, i.e., `μ m n₁ < μ m n₂` whenever `n₁ < n₂` for any `m`, is equivalent to the property that `μ` is contravariant with respect to the "less than or equal to" relation, i.e., if `μ m n₁ ≤ μ m n₂` then `n₁ ≤ n₂` for any `m`. This is a statement about the preservation of order relations under the action of a function from some type onto another type.
More concisely: For any function `μ` from type `M` to type `N` and linear order on `N`, `μ` is covariant with respect to the "less than" relation if and only if it is contravariant with respect to the "less than or equal to" relation, i.e., `μ m n₁ < μ m n₂` if and only if `n₁ ≤ n₂` for all `m`.
|
covariant_le_iff_contravariant_lt
theorem covariant_le_iff_contravariant_lt :
∀ (M : Type u_1) (N : Type u_2) (μ : M → N → N) [inst : LinearOrder N],
(Covariant M N μ fun x x_1 => x ≤ x_1) ↔ Contravariant M N μ fun x x_1 => x < x_1
This theorem, `covariant_le_iff_contravariant_lt`, is a universal statement for any two types `M` and `N`, and a function `μ` from `M` and `N` to `N`. It states that if `N` has a linear order, then the function `μ` is covariant with respect to the less than or equal to relation (i.e., if `n₁ ≤ n₂`, then `μ m n₁ ≤ μ m n₂` for all `m` in `M`) if and only if `μ` is contravariant with respect to the strictly less than relation (i.e., if `μ m n₁ < μ m n₂`, then `n₁ < n₂` for all `m` in `M`). Essentially, this theorem establishes a connection between the covariance of `μ` regarding the "less than or equal to" relation and its contravariance regarding the "strictly less than" relation in the context of a linear order.
More concisely: For any functions `μ` from type `M` to type `N` over a linearly ordered type `N`, `μ` is covariant with respect to the less than or equal to relation if and only if it is contravariant with respect to the strict less than relation.
|
Monotone.covariant_of_const'
theorem Monotone.covariant_of_const' :
∀ {N : Type u_2} {α : Type u_3} [inst : Preorder α] [inst_1 : Preorder N] {f : N → α} {μ : N → N → N}
[inst_2 : CovariantClass N N (Function.swap μ) fun x x_1 => x ≤ x_1],
Monotone f → ∀ (m : N), Monotone fun x => f (μ x m)
The theorem `Monotone.covariant_of_const'` states that for any types `N` and `α`, both equipped with a preorder relation, a function `f : N → α`, and a binary operation `μ : N → N → N`, if `μ` behaves covariantly with respect to the preorder relation (i.e., if `x ≤ y` then `μ x z ≤ μ y z` for all `z`), and if `f` is a monotone function (i.e., if `a ≤ b` then `f(a) ≤ f(b)`), then for any fixed value `m : N`, the function `x ↦ f (μ x m)` is also monotone. In other words, applying `f` after performing the operation `μ` with a constant argument does not break the monotonicity of `f`.
More concisely: If `μ : N → N → N` covariantly respects a preorder relation on `N` and `f : N → α` is a monotone function, then the function `x ↦ f (μ x m)` is monotone for any constant `m : N`.
|
act_rel_act_of_rel
theorem act_rel_act_of_rel :
∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : CovariantClass M N μ r] (m : M)
{a b : N}, r a b → r (μ m a) (μ m b)
This theorem states that for any types `M` and `N`, a binary operation `μ` from `M` and `N` to `N`, and a binary relation `r` on `N`, given that `μ` is a covariant with respect to `r`, and for any element `m` of type `M` and any elements `a` and `b` of type `N`, if `r` holds between `a` and `b`, then `r` also holds between `μ(m, a)` and `μ(m, b)`. Essentially, if `a` and `b` are related under `r`, then applying the operation `μ` with `m` to `a` and `b` will also produce two elements that are related under `r`. It's a property about preserving the relational structure under the operation `μ`.
More concisely: If `μ` is a covariant binary operation from types `M` and `N` to `N`, and `r` is a relation on `N` such that `r(μ(m, a), μ(m, b))` holds whenever `r(a, b)` does, then `μ` preserves `r`.
|
CovariantClass.elim
theorem CovariantClass.elim :
∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [self : CovariantClass M N μ r],
Covariant M N μ r
The theorem `CovariantClass.elim` states that, given any types `M` and `N`, a binary function `\mu` from `M` and `N` to `N`, and a binary relation `r` on `N`, if the `CovariantClass` of `M`, `N`, `\mu`, and `r` exists, then it satisfies the property of covariance. Concretely, for any element `m` from `M` and any elements `n₁`, `n₂` from `N`, if the relation `r` holds between `n₁` and `n₂`, then the relation `r` also holds between `\mu m n₁` and `\mu m n₂`. This is a key property of functions and relations that interact covariantly.
More concisely: Given functions `μ : M → N`, relation `r : N × N → Prop`, and assuming the existence of the CovariantClass of `M`, `N`, `μ`, and `r`, if `r (n₁, n₂)` holds, then `r (μ x n₁)` and `r (μ x n₂)` hold for all `x : M`.
|
Antitone.covariant_of_const
theorem Antitone.covariant_of_const :
∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {α : Type u_3} [inst : Preorder α] [inst_1 : Preorder N] {f : N → α}
[inst_2 : CovariantClass M N μ fun x x_1 => x ≤ x_1], Antitone f → ∀ (m : M), Antitone fun x => f (μ m x)
The theorem `Antitone.covariant_of_const` states that for any types `M`, `N`, and `α`, and for any function `μ` from `M` and `N` to `N`, if `α` and `N` are preordered, if `f` is a function from `N` to `α`, if `μ` is covariant (i.e., if for all `x` and `x_1` in `N`, `x ≤ x_1` implies `μ m x ≤ μ m x_1` for any `m` in `M`), and if `f` is antitone (i.e., if for all `a` and `b` in `α`, `a ≤ b` implies `f(b) ≤ f(a)`), then for any `m` in `M`, the function that maps `x` in `N` to `f(μ(m, x))` is also antitone.
More concisely: If `μ: M -> N -> N`, `α` is preordered, `f: N -> α` is antitone and covariant with respect to `μ`, then the function `x => f(μ(m, x))` is antitone for any `m: M`.
|
Covariant.monotone_of_const
theorem Covariant.monotone_of_const :
∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} [inst : Preorder N]
[inst_1 : CovariantClass M N μ fun x x_1 => x ≤ x_1] (m : M), Monotone (μ m)
The theorem `Covariant.monotone_of_const` states that for any two types `M` and `N`, a function `μ` from `M` to `N` to `N`, a preorder on `N`, and when `μ` is a covariant operator (meaning it respects the order), partially applying a constant `m` from `M` to the function `μ` results in a function that is monotone. In other words, if `a ≤ b`, then `μ m a ≤ μ m b`. This means that as the input to the partially applied function increases, the output also increases.
More concisely: For any covariant function `μ` from type `M` to a preorder `N`, and constant `m` from `M`, the function `μ m : N` is monotone, i.e., for all `a ≤ b` in `M`, `μ m a ≤ μ m b` holds in `N`.
|
covariantClass_le_of_lt
theorem covariantClass_le_of_lt :
∀ (M : Type u_1) (N : Type u_2) (μ : M → N → N) [inst : PartialOrder N]
[inst_1 : CovariantClass M N μ fun x x_1 => x < x_1], CovariantClass M N μ fun x x_1 => x ≤ x_1
This theorem states that for any two types `M` and `N` and a function `μ` from `M` to `N` to `N`, if `N` has a partial order and `μ` is a covariant class with respect to a strict order (`<`), then `μ` is also a covariant class with respect to a nonstrict order (`≤`). In other words, if the function `μ` preserves the strict order of elements in `N` when applied with elements from `M`, it also preserves the nonstrict order.
More concisely: If `μ` is a covariant function from type `M` to type `N` with respect to the strict order `<` on `N`, then it is also covariant with respect to the non-strict order `≤` on `N`.
|