Covariants and contravariants

This file contains general lemmas and instances to work with the interactions between a relation and an action on a Type.

The intended application is the splitting of the ordering from the algebraic assumptions on the operations in the Ordered[...] hierarchy.

The strategy is to introduce two more flexible typeclasses, CovariantClass and ContravariantClass:

• CovariantClass models the implication a ≤ b → c * a ≤ c * b (multiplication is monotone),
• ContravariantClass models the implication a * b < a * c → b < c.

Since Co(ntra)variantClass takes as input the operation (typically (+) or (*)) and the order relation (typically (≤) or (<)), these are the only two typeclasses that I have used.

The general approach is to formulate the lemma that you are interested in and prove it, with the Ordered[...] typeclass of your liking. After that, you convert the single typeclass, say [OrderedCancelMonoid M], into three typeclasses, e.g. [CancelMonoid M] [PartialOrder M] [CovariantClass M M (Function.swap (*)) (≤)] and have a go at seeing if the proof still works!

Note that it is possible to combine several Co(ntra)variantClass assumptions together. Indeed, the usual ordered typeclasses arise from assuming the pair [CovariantClass M M (*) (≤)] [ContravariantClass M M (*) (<)] on top of order/algebraic assumptions.

A formal remark is that normally CovariantClass uses the (≤)-relation, while ContravariantClass uses the (<)-relation. This need not be the case in general, but seems to be the most common usage. In the opposite direction, the implication

[Semigroup α] [PartialOrder α] [ContravariantClass α α (*) (≤)] → LeftCancelSemigroup α

holds -- note the Co*ntra* assumption on the (≤)-relation.

Formalization notes

We stick to the convention of using Function.swap (*) (or Function.swap (+)), for the typeclass assumptions, since Function.swap is slightly better behaved than flip. However, sometimes as a non-typeclass assumption, we prefer flip (*) (or flip (+)), as it is easier to use.

def Covariant (M : Type u_1) (N : Type u_2) (μ : M → N → N) (r : N → N → Prop) : Prop

Covariant is useful to formulate succinctly statements about the interactions between an action of a Type on another one and a relation on the acted-upon Type.

See the CovariantClass doc-string for its meaning.

Equations

• Covariant M N μ r = ∀ (m : M) {n₁ n₂ : N}, r n₁ n₂ → r (μ m n₁) (μ m n₂)

def Contravariant (M : Type u_1) (N : Type u_2) (μ : M → N → N) (r : N → N → Prop) : Prop

Contravariant is useful to formulate succinctly statements about the interactions between an action of a Type on another one and a relation on the acted-upon Type.

See the ContravariantClass doc-string for its meaning.

Equations

• Contravariant M N μ r = ∀ (m : M) {n₁ n₂ : N}, r (μ m n₁) (μ m n₂) → r n₁ n₂

class CovariantClass (M : Type u_1) (N : Type u_2) (μ : M → N → N) (r : N → N → Prop) : Prop

Given an action μ of a Type M on a Type N and a relation r on N, informally, the CovariantClass says that "the action μ preserves the relation r."

More precisely, the CovariantClass is a class taking two Types M N, together with an "action" μ : M → N → N and a relation r : N → N → Prop. Its unique field elim is the assertion that for all m ∈ M and all elements n₁, n₂ ∈ N, if the relation r holds for the pair (n₁, n₂), then, the relation r also holds for the pair (μ m n₁, μ m n₂), obtained from (n₁, n₂) by acting upon it by m.

If m : M and h : r n₁ n₂, then CovariantClass.elim m h : r (μ m n₁) (μ m n₂).

• elim : Covariant M N μ r

  For all m ∈ M and all elements n₁, n₂ ∈ N, if the relation r holds for the pair (n₁, n₂), then, the relation r also holds for the pair (μ m n₁, μ m n₂)

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

For all m ∈ M and all elements n₁, n₂ ∈ N, if the relation r holds for the pair (n₁, n₂), then, the relation r also holds for the pair (μ m n₁, μ m n₂)

class ContravariantClass (M : Type u_1) (N : Type u_2) (μ : M → N → N) (r : N → N → Prop) : Prop

Given an action μ of a Type M on a Type N and a relation r on N, informally, the ContravariantClass says that "if the result of the action μ on a pair satisfies the relation r, then the initial pair satisfied the relation r."

More precisely, the ContravariantClass is a class taking two Types M N, together with an "action" μ : M → N → N and a relation r : N → N → Prop. Its unique field elim is the assertion that for all m ∈ M and all elements n₁, n₂ ∈ N, if the relation r holds for the pair (μ m n₁, μ m n₂) obtained from (n₁, n₂) by acting upon it by m, then, the relation r also holds for the pair (n₁, n₂).

If m : M and h : r (μ m n₁) (μ m n₂), then ContravariantClass.elim m h : r n₁ n₂.

• elim : Contravariant M N μ r

  For all m ∈ M and all elements n₁, n₂ ∈ N, if the relation r holds for the pair (μ m n₁, μ m n₂) obtained from (n₁, n₂) by acting upon it by m, then, the relation r also holds for the pair (n₁, n₂).

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

For all m ∈ M and all elements n₁, n₂ ∈ N, if the relation r holds for the pair (μ m n₁, μ m n₂) obtained from (n₁, n₂) by acting upon it by m, then, the relation r also holds for the pair (n₁, n₂).

@[reducible, inline]

abbrev MulLeftMono (M : Type u_1) [Mul M] [LE M] : Prop

Typeclass for monotonicity of multiplication on the left, namely b₁ ≤ b₂ → a * b₁ ≤ a * b₂.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedCommMonoid.

Equations

• MulLeftMono M = CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2

@[reducible, inline]

abbrev MulRightMono (M : Type u_1) [Mul M] [LE M] : Prop

Typeclass for monotonicity of multiplication on the right, namely a₁ ≤ a₂ → a₁ * b ≤ a₂ * b.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedCommMonoid.

Equations

• MulRightMono M = CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2

@[reducible, inline]

abbrev AddLeftMono (M : Type u_1) [Add M] [LE M] : Prop

Typeclass for monotonicity of addition on the left, namely b₁ ≤ b₂ → a + b₁ ≤ a + b₂.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedAddCommMonoid.

Equations

• AddLeftMono M = CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2

@[reducible, inline]

abbrev AddRightMono (M : Type u_1) [Add M] [LE M] : Prop

Typeclass for monotonicity of addition on the right, namely a₁ ≤ a₂ → a₁ + b ≤ a₂ + b.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedAddCommMonoid.

Equations

• AddRightMono M = CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2

@[reducible, inline]

abbrev MulLeftStrictMono (M : Type u_1) [Mul M] [LT M] : Prop

Typeclass for monotonicity of multiplication on the left, namely b₁ < b₂ → a * b₁ < a * b₂.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedCommGroup.

Equations

• MulLeftStrictMono M = CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 < x2

@[reducible, inline]

abbrev MulRightStrictMono (M : Type u_1) [Mul M] [LT M] : Prop

Typeclass for monotonicity of multiplication on the right, namely a₁ < a₂ → a₁ * b < a₂ * b.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedCommGroup.

Equations

• MulRightStrictMono M = CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 < x2

@[reducible, inline]

abbrev AddLeftStrictMono (M : Type u_1) [Add M] [LT M] : Prop

Typeclass for monotonicity of addition on the left, namely b₁ < b₂ → a + b₁ < a + b₂.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedAddCommGroup.

Equations

• AddLeftStrictMono M = CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2

@[reducible, inline]

abbrev AddRightStrictMono (M : Type u_1) [Add M] [LT M] : Prop

Typeclass for monotonicity of addition on the right, namely a₁ < a₂ → a₁ + b < a₂ + b.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedAddCommGroup.

Equations

• AddRightStrictMono M = CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2

@[reducible, inline]

abbrev MulLeftReflectLT (M : Type u_1) [Mul M] [LT M] : Prop

Typeclass for strict reverse monotonicity of multiplication on the left, namely a * b₁ < a * b₂ → b₁ < b₂.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedCommGroup.

Equations

• MulLeftReflectLT M = ContravariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 < x2

@[reducible, inline]

abbrev MulRightReflectLT (M : Type u_1) [Mul M] [LT M] : Prop

Typeclass for strict reverse monotonicity of multiplication on the right, namely a₁ * b < a₂ * b → a₁ < a₂.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedCommGroup.

Equations

• MulRightReflectLT M = ContravariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 < x2

@[reducible, inline]

abbrev AddLeftReflectLT (M : Type u_1) [Add M] [LT M] : Prop

Typeclass for strict reverse monotonicity of addition on the left, namely a + b₁ < a + b₂ → b₁ < b₂.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedAddCommGroup.

Equations

• AddLeftReflectLT M = ContravariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2

@[reducible, inline]

abbrev AddRightReflectLT (M : Type u_1) [Add M] [LT M] : Prop

Typeclass for strict reverse monotonicity of addition on the right, namely a₁ * b < a₂ * b → a₁ < a₂.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedAddCommGroup.

Equations

• AddRightReflectLT M = ContravariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2

@[reducible, inline]

abbrev MulLeftReflectLE (M : Type u_1) [Mul M] [LE M] : Prop

Typeclass for reverse monotonicity of multiplication on the left, namely a * b₁ ≤ a * b₂ → b₁ ≤ b₂.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedCancelCommMonoid.

Equations

• MulLeftReflectLE M = ContravariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2

@[reducible, inline]

abbrev MulRightReflectLE (M : Type u_1) [Mul M] [LE M] : Prop

Typeclass for reverse monotonicity of multiplication on the right, namely a₁ * b ≤ a₂ * b → a₁ ≤ a₂.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedCancelCommMonoid.

Equations

• MulRightReflectLE M = ContravariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2

@[reducible, inline]

abbrev AddLeftReflectLE (M : Type u_1) [Add M] [LE M] : Prop

Typeclass for reverse monotonicity of addition on the left, namely a + b₁ ≤ a + b₂ → b₁ ≤ b₂.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedCancelAddCommMonoid.

Equations

• AddLeftReflectLE M = ContravariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2

@[reducible, inline]

abbrev AddRightReflectLE (M : Type u_1) [Add M] [LE M] : Prop

Typeclass for reverse monotonicity of addition on the right, namely a₁ + b ≤ a₂ + b → a₁ ≤ a₂.

You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedCancelAddCommMonoid.

Equations

• AddRightReflectLE M = ContravariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2

theorem rel_iff_cov (M : Type u_1) (N : Type u_2) (μ : M → N → N) (r : N → N → Prop) [CovariantClass M N μ r] [ContravariantClass M N μ r] (m : M) {a : N} {b : N} : r (μ m a) (μ m b) ↔ r a b

theorem Covariant.flip {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} (h : Covariant M N μ r) : Covariant M N μ (flip r)

theorem Contravariant.flip {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} (h : Contravariant M N μ r) : Contravariant M N μ (flip r)

theorem act_rel_act_of_rel {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [CovariantClass M N μ r] (m : M) {a : N} {b : N} (ab : r a b) : r (μ m a) (μ m b)

theorem AddGroup.covariant_iff_contravariant {N : Type u_2} {r : N → N → Prop} [AddGroup N] : Covariant N N (fun (x1 x2 : N) => x1 + x2) r ↔ Contravariant N N (fun (x1 x2 : N) => x1 + x2) r

theorem Group.covariant_iff_contravariant {N : Type u_2} {r : N → N → Prop} [Group N] : Covariant N N (fun (x1 x2 : N) => x1 * x2) r ↔ Contravariant N N (fun (x1 x2 : N) => x1 * x2) r

@[instance 100]

instance AddGroup.covconv {N : Type u_2} {r : N → N → Prop} [AddGroup N] [CovariantClass N N (fun (x1 x2 : N) => x1 + x2) r] : ContravariantClass N N (fun (x1 x2 : N) => x1 + x2) r

Equations

• ⋯ = ⋯

@[instance 100]

instance Group.covconv {N : Type u_2} {r : N → N → Prop} [Group N] [CovariantClass N N (fun (x1 x2 : N) => x1 * x2) r] : ContravariantClass N N (fun (x1 x2 : N) => x1 * x2) r

Equations

• ⋯ = ⋯

theorem AddGroup.addLeftReflectLE_of_addLeftMono {N : Type u_2} [AddGroup N] [LE N] [AddLeftMono N] : AddLeftReflectLE N

theorem Group.mulLeftReflectLE_of_mulLeftMono {N : Type u_2} [Group N] [LE N] [MulLeftMono N] : MulLeftReflectLE N

theorem AddGroup.addLeftReflectLT_of_addLeftStrictMono {N : Type u_2} [AddGroup N] [LT N] [AddLeftStrictMono N] : AddLeftReflectLT N

theorem Group.mulLeftReflectLT_of_mulLeftStrictMono {N : Type u_2} [Group N] [LT N] [MulLeftStrictMono N] : MulLeftReflectLT N

theorem AddGroup.covariant_swap_iff_contravariant_swap {N : Type u_2} {r : N → N → Prop} [AddGroup N] : Covariant N N (Function.swap fun (x1 x2 : N) => x1 + x2) r ↔ Contravariant N N (Function.swap fun (x1 x2 : N) => x1 + x2) r

theorem Group.covariant_swap_iff_contravariant_swap {N : Type u_2} {r : N → N → Prop} [Group N] : Covariant N N (Function.swap fun (x1 x2 : N) => x1 * x2) r ↔ Contravariant N N (Function.swap fun (x1 x2 : N) => x1 * x2) r

@[instance 100]

instance AddGroup.covconv_swap {N : Type u_2} {r : N → N → Prop} [AddGroup N] [CovariantClass N N (Function.swap fun (x1 x2 : N) => x1 + x2) r] : ContravariantClass N N (Function.swap fun (x1 x2 : N) => x1 + x2) r

Equations

• ⋯ = ⋯

@[instance 100]

instance Group.covconv_swap {N : Type u_2} {r : N → N → Prop} [Group N] [CovariantClass N N (Function.swap fun (x1 x2 : N) => x1 * x2) r] : ContravariantClass N N (Function.swap fun (x1 x2 : N) => x1 * x2) r

Equations

• ⋯ = ⋯

theorem AddGroup.addRightReflectLE_of_addRightMono {N : Type u_2} [AddGroup N] [LE N] [AddRightMono N] : AddRightReflectLE N

theorem Group.mulRightReflectLE_of_mulRightMono {N : Type u_2} [Group N] [LE N] [MulRightMono N] : MulRightReflectLE N

theorem AddGroup.addRightReflectLT_of_addRightStrictMono {N : Type u_2} [AddGroup N] [LT N] [AddRightStrictMono N] : AddRightReflectLT N

theorem Group.mulRightReflectLT_of_mulRightStrictMono {N : Type u_2} [Group N] [LT N] [MulRightStrictMono N] : MulRightReflectLT N

theorem act_rel_of_rel_of_act_rel {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [CovariantClass M N μ r] [IsTrans N r] (m : M) {a : N} {b : N} {c : N} (ab : r a b) (rl : r (μ m b) c) : r (μ m a) c

theorem rel_act_of_rel_of_rel_act {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [CovariantClass M N μ r] [IsTrans N r] (m : M) {a : N} {b : N} {c : N} (ab : r a b) (rr : r c (μ m a)) : r c (μ m b)

theorem act_rel_act_of_rel_of_rel {N : Type u_2} {r : N → N → Prop} {mu : N → N → N} [IsTrans N r] [i : CovariantClass N N mu r] [i' : CovariantClass N N (Function.swap mu) r] {a : N} {b : N} {c : N} {d : N} (ab : r a b) (cd : r c d) : r (mu a c) (mu b d)

theorem rel_of_act_rel_act {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [ContravariantClass M N μ r] (m : M) {a : N} {b : N} (ab : r (μ m a) (μ m b)) : r a b

theorem act_rel_of_act_rel_of_rel_act_rel {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [ContravariantClass M N μ r] [IsTrans N r] (m : M) {a : N} {b : N} {c : N} (ab : r (μ m a) b) (rl : r (μ m b) (μ m c)) : r (μ m a) c

theorem rel_act_of_act_rel_act_of_rel_act {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [ContravariantClass M N μ r] [IsTrans N r] (m : M) {a : N} {b : N} {c : N} (ab : r (μ m a) (μ m b)) (rr : r b (μ m c)) : r a (μ m c)

theorem Covariant.monotone_of_const {M : Type u_1} {N : Type u_2} {μ : M → N → N} [Preorder N] [CovariantClass M N μ fun (x1 x2 : N) => x1 ≤ x2] (m : M) : Monotone (μ m)

The partial application of a constant to a covariant operator is monotone.

theorem Monotone.covariant_of_const {M : Type u_1} {N : Type u_2} {μ : M → N → N} {α : Type u_3} [Preorder α] [Preorder N] {f : N → α} [CovariantClass M N μ fun (x1 x2 : N) => x1 ≤ x2] (hf : Monotone f) (m : M) : Monotone fun (x : N) => f (μ m x)

A monotone function remains monotone when composed with the partial application of a covariant operator. E.g., ∀ (m : ℕ), Monotone f → Monotone (fun n ↦ f (m + n)).

theorem Monotone.covariant_of_const' {N : Type u_2} {α : Type u_3} [Preorder α] [Preorder N] {f : N → α} {μ : N → N → N} [CovariantClass N N (Function.swap μ) fun (x1 x2 : N) => x1 ≤ x2] (hf : Monotone f) (m : N) : Monotone fun (x : N) => f (μ x m)

Same as Monotone.covariant_of_const, but with the constant on the other side of the operator. E.g., ∀ (m : ℕ), Monotone f → Monotone (fun n ↦ f (n + m)).

theorem Antitone.covariant_of_const {M : Type u_1} {N : Type u_2} {μ : M → N → N} {α : Type u_3} [Preorder α] [Preorder N] {f : N → α} [CovariantClass M N μ fun (x1 x2 : N) => x1 ≤ x2] (hf : Antitone f) (m : M) : Antitone fun (x : N) => f (μ m x)

Dual of Monotone.covariant_of_const

theorem Antitone.covariant_of_const' {N : Type u_2} {α : Type u_3} [Preorder α] [Preorder N] {f : N → α} {μ : N → N → N} [CovariantClass N N (Function.swap μ) fun (x1 x2 : N) => x1 ≤ x2] (hf : Antitone f) (m : N) : Antitone fun (x : N) => f (μ x m)

Dual of Monotone.covariant_of_const'

theorem covariant_le_of_covariant_lt (M : Type u_1) (N : Type u_2) (μ : M → N → N) [PartialOrder N] : (Covariant M N μ fun (x1 x2 : N) => x1 < x2) → Covariant M N μ fun (x1 x2 : N) => x1 ≤ x2

theorem covariantClass_le_of_lt (M : Type u_1) (N : Type u_2) (μ : M → N → N) [PartialOrder N] [CovariantClass M N μ fun (x1 x2 : N) => x1 < x2] : CovariantClass M N μ fun (x1 x2 : N) => x1 ≤ x2

theorem addLeftMono_of_addLeftStrictMono (M : Type u_3) [Add M] [PartialOrder M] [AddLeftStrictMono M] : AddLeftMono M

theorem mulLeftMono_of_mulLeftStrictMono (M : Type u_3) [Mul M] [PartialOrder M] [MulLeftStrictMono M] : MulLeftMono M

theorem addRightMono_of_addRightStrictMono (M : Type u_3) [Add M] [PartialOrder M] [AddRightStrictMono M] : AddRightMono M

theorem mulRightMono_of_mulRightStrictMono (M : Type u_3) [Mul M] [PartialOrder M] [MulRightStrictMono M] : MulRightMono M

theorem contravariant_le_iff_contravariant_lt_and_eq (M : Type u_1) (N : Type u_2) (μ : M → N → N) [PartialOrder N] : (Contravariant M N μ fun (x1 x2 : N) => x1 ≤ x2) ↔ (Contravariant M N μ fun (x1 x2 : N) => x1 < x2) ∧ Contravariant M N μ fun (x1 x2 : N) => x1 = x2

theorem contravariant_lt_of_contravariant_le (M : Type u_1) (N : Type u_2) (μ : M → N → N) [PartialOrder N] : (Contravariant M N μ fun (x1 x2 : N) => x1 ≤ x2) → Contravariant M N μ fun (x1 x2 : N) => x1 < x2

theorem covariant_le_iff_contravariant_lt (M : Type u_1) (N : Type u_2) (μ : M → N → N) [LinearOrder N] : (Covariant M N μ fun (x1 x2 : N) => x1 ≤ x2) ↔ Contravariant M N μ fun (x1 x2 : N) => x1 < x2

theorem covariant_lt_iff_contravariant_le (M : Type u_1) (N : Type u_2) (μ : M → N → N) [LinearOrder N] : (Covariant M N μ fun (x1 x2 : N) => x1 < x2) ↔ Contravariant M N μ fun (x1 x2 : N) => x1 ≤ x2

theorem covariant_flip_iff (N : Type u_2) (r : N → N → Prop) (mu : N → N → N) [h : Std.Commutative mu] : Covariant N N (flip mu) r ↔ Covariant N N mu r

theorem contravariant_flip_iff (N : Type u_2) (r : N → N → Prop) (mu : N → N → N) [h : Std.Commutative mu] : Contravariant N N (flip mu) r ↔ Contravariant N N mu r

instance contravariant_lt_of_covariant_le (N : Type u_2) (mu : N → N → N) [LinearOrder N] [CovariantClass N N mu fun (x1 x2 : N) => x1 ≤ x2] : ContravariantClass N N mu fun (x1 x2 : N) => x1 < x2

Equations

• ⋯ = ⋯

theorem addLeftReflectLT_of_addLeftMono (N : Type u_2) [Add N] [LinearOrder N] [AddLeftMono N] : AddLeftReflectLT N

theorem mulLeftReflectLT_of_mulLeftMono (N : Type u_2) [Mul N] [LinearOrder N] [MulLeftMono N] : MulLeftReflectLT N

theorem addRightReflectLT_of_addRightMono (N : Type u_2) [Add N] [LinearOrder N] [AddRightMono N] : AddRightReflectLT N

theorem mulRightReflectLT_of_mulRightMono (N : Type u_2) [Mul N] [LinearOrder N] [MulRightMono N] : MulRightReflectLT N

instance covariant_lt_of_contravariant_le (N : Type u_2) (mu : N → N → N) [LinearOrder N] [ContravariantClass N N mu fun (x1 x2 : N) => x1 ≤ x2] : CovariantClass N N mu fun (x1 x2 : N) => x1 < x2

Equations

• ⋯ = ⋯

theorem addLeftStrictMono_of_addLeftReflectLE (N : Type u_2) [Add N] [LinearOrder N] [AddLeftReflectLE N] : AddLeftStrictMono N

theorem mulLeftStrictMono_of_mulLeftReflectLE (N : Type u_2) [Mul N] [LinearOrder N] [MulLeftReflectLE N] : MulLeftStrictMono N

theorem addRightStrictMono_of_addRightReflectLE (N : Type u_2) [Add N] [LinearOrder N] [AddRightReflectLE N] : AddRightStrictMono N

theorem mulRightStrictMono_of_mulRightReflectLE (N : Type u_2) [Mul N] [LinearOrder N] [MulRightReflectLE N] : MulRightStrictMono N

instance covariant_swap_add_of_covariant_add (N : Type u_2) (r : N → N → Prop) [AddCommSemigroup N] [CovariantClass N N (fun (x1 x2 : N) => x1 + x2) r] : CovariantClass N N (Function.swap fun (x1 x2 : N) => x1 + x2) r

Equations

• ⋯ = ⋯

instance covariant_swap_mul_of_covariant_mul (N : Type u_2) (r : N → N → Prop) [CommSemigroup N] [CovariantClass N N (fun (x1 x2 : N) => x1 * x2) r] : CovariantClass N N (Function.swap fun (x1 x2 : N) => x1 * x2) r

Equations

• ⋯ = ⋯

theorem addRightMono_of_addLeftMono (N : Type u_2) [AddCommSemigroup N] [LE N] [AddLeftMono N] : AddRightMono N

theorem mulRightMono_of_mulLeftMono (N : Type u_2) [CommSemigroup N] [LE N] [MulLeftMono N] : MulRightMono N

theorem addRightStrictMono_of_addLeftStrictMono (N : Type u_2) [AddCommSemigroup N] [LT N] [AddLeftStrictMono N] : AddRightStrictMono N

theorem mulRightStrictMono_of_mulLeftStrictMono (N : Type u_2) [CommSemigroup N] [LT N] [MulLeftStrictMono N] : MulRightStrictMono N

instance contravariant_swap_add_of_contravariant_add (N : Type u_2) (r : N → N → Prop) [AddCommSemigroup N] [ContravariantClass N N (fun (x1 x2 : N) => x1 + x2) r] : ContravariantClass N N (Function.swap fun (x1 x2 : N) => x1 + x2) r

Equations

• ⋯ = ⋯

instance contravariant_swap_mul_of_contravariant_mul (N : Type u_2) (r : N → N → Prop) [CommSemigroup N] [ContravariantClass N N (fun (x1 x2 : N) => x1 * x2) r] : ContravariantClass N N (Function.swap fun (x1 x2 : N) => x1 * x2) r

Equations

• ⋯ = ⋯

theorem addRightReflectLE_of_addLeftReflectLE (N : Type u_2) [AddCommSemigroup N] [LE N] [AddLeftReflectLE N] : AddRightReflectLE N

theorem mulRightReflectLE_of_mulLeftReflectLE (N : Type u_2) [CommSemigroup N] [LE N] [MulLeftReflectLE N] : MulRightReflectLE N

theorem addRightReflectLT_of_addLeftReflectLT (N : Type u_2) [AddCommSemigroup N] [LT N] [AddLeftReflectLT N] : AddRightReflectLT N

theorem mulRightReflectLT_of_mulLeftReflectLT (N : Type u_2) [CommSemigroup N] [LT N] [MulLeftReflectLT N] : MulRightReflectLT N

theorem covariant_lt_of_covariant_le_of_contravariant_eq (M : Type u_1) (N : Type u_2) (μ : M → N → N) [ContravariantClass M N μ fun (x1 x2 : N) => x1 = x2] [PartialOrder N] [CovariantClass M N μ fun (x1 x2 : N) => x1 ≤ x2] : CovariantClass M N μ fun (x1 x2 : N) => x1 < x2

theorem contravariant_le_of_contravariant_eq_and_lt (M : Type u_1) (N : Type u_2) (μ : M → N → N) [PartialOrder N] [ContravariantClass M N μ fun (x1 x2 : N) => x1 = x2] [ContravariantClass M N μ fun (x1 x2 : N) => x1 < x2] : ContravariantClass M N μ fun (x1 x2 : N) => x1 ≤ x2

instance IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono (N : Type u_2) [Add N] [IsLeftCancelAdd N] [PartialOrder N] [AddLeftMono N] : AddLeftStrictMono N

Equations

• ⋯ = ⋯

instance IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono (N : Type u_2) [Mul N] [IsLeftCancelMul N] [PartialOrder N] [MulLeftMono N] : MulLeftStrictMono N

Equations

• ⋯ = ⋯

instance IsRightCancelAdd.addRightStrictMono_of_addRightMono (N : Type u_2) [Add N] [IsRightCancelAdd N] [PartialOrder N] [AddRightMono N] : AddRightStrictMono N

Equations

• ⋯ = ⋯

instance IsRightCancelMul.mulRightStrictMono_of_mulRightMono (N : Type u_2) [Mul N] [IsRightCancelMul N] [PartialOrder N] [MulRightMono N] : MulRightStrictMono N

Equations

• ⋯ = ⋯

instance IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT (N : Type u_2) [Add N] [IsLeftCancelAdd N] [PartialOrder N] [AddLeftReflectLT N] : AddLeftReflectLE N

Equations

• ⋯ = ⋯

instance IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT (N : Type u_2) [Mul N] [IsLeftCancelMul N] [PartialOrder N] [MulLeftReflectLT N] : MulLeftReflectLE N

Equations

• ⋯ = ⋯

instance IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT (N : Type u_2) [Add N] [IsRightCancelAdd N] [PartialOrder N] [AddRightReflectLT N] : AddRightReflectLE N

Equations

• ⋯ = ⋯

instance IsRightCancelMul.mulRightReflectLE_of_mulRightReflectLT (N : Type u_2) [Mul N] [IsRightCancelMul N] [PartialOrder N] [MulRightReflectLT N] : MulRightReflectLE N

Equations

• ⋯ = ⋯