Documentation

Mathlib.Algebra.CovariantAndContravariant

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≤ b → c * a ≤ c * b→ c * a ≤ c * b≤ c * b (multiplication is monotone),
ContravariantClass models the implication a * b < a * c → b < 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. [LeftCancelSemigroup 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 (*) (<)]≤)] [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 α
≤)] => 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) :

Covariant is useful to formulate succintly 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) :

Contravariant is useful to formulate succintly 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) :

For all m ∈ M∈ M and all elements n₁, 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₂)
elim : Covariant M N μ r

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→ N → N→ N and a relation r : N → N → Prop→ N → Prop→ Prop. Its unique field elim is the assertion that for all m ∈ M∈ M and all elements n₁, 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₂).

Instances

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

For all m ∈ M∈ M and all elements n₁, 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₂).
elim : Contravariant M N μ r

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→ N → N→ N and a relation r : N → N → Prop→ N → Prop→ Prop. Its unique field elim is the assertion that for all m ∈ M∈ M and all elements n₁, 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₂.

Instances

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 : 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} [inst : 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_1} {r : N → N → Prop} [inst : AddGroup N] :

Covariant N N (fun x x_1 => x + x_1) r ↔ Contravariant N N (fun x x_1 => x + x_1) r

theorem Group.covariant_iff_contravariant {N : Type u_1} {r : N → N → Prop} [inst : Group N] :

Covariant N N (fun x x_1 => x * x_1) r ↔ Contravariant N N (fun x x_1 => x * x_1) r

def AddGroup.covconv.proof_1 {N : Type u_1} {r : N → N → Prop} [inst : AddGroup N] [inst : CovariantClass N N (fun x x_1 => x + x_1) r] :

ContravariantClass N N (fun x x_1 => x + x_1) r

Equations

(_ : ContravariantClass N N (fun x x_1 => x + x_1) r) = (_ : ContravariantClass N N (fun x x_1 => x + x_1) r)

instance AddGroup.covconv {N : Type u_1} {r : N → N → Prop} [inst : AddGroup N] [inst : CovariantClass N N (fun x x_1 => x + x_1) r] :

ContravariantClass N N (fun x x_1 => x + x_1) r

Equations

@AddGroup.covconv = @AddGroup.covconv.proof_1

instance Group.covconv {N : Type u_1} {r : N → N → Prop} [inst : Group N] [inst : CovariantClass N N (fun x x_1 => x * x_1) r] :

ContravariantClass N N (fun x x_1 => x * x_1) r

Equations

@Group.covconv = @Group.covconv.proof_1

theorem AddGroup.covariant_swap_iff_contravariant_swap {N : Type u_1} {r : N → N → Prop} [inst : AddGroup N] :

Covariant N N (Function.swap fun x x_1 => x + x_1) r ↔ Contravariant N N (Function.swap fun x x_1 => x + x_1) r

theorem Group.covariant_swap_iff_contravariant_swap {N : Type u_1} {r : N → N → Prop} [inst : Group N] :

Covariant N N (Function.swap fun x x_1 => x * x_1) r ↔ Contravariant N N (Function.swap fun x x_1 => x * x_1) r

def AddGroup.covconv_swap.proof_1 {N : Type u_1} {r : N → N → Prop} [inst : AddGroup N] [inst : CovariantClass N N (Function.swap fun x x_1 => x + x_1) r] :

ContravariantClass N N (Function.swap fun x x_1 => x + x_1) r

Equations

(_ : ContravariantClass N N (Function.swap fun x x_1 => x + x_1) r) = (_ : ContravariantClass N N (Function.swap fun x x_1 => x + x_1) r)

instance AddGroup.covconv_swap {N : Type u_1} {r : N → N → Prop} [inst : AddGroup N] [inst : CovariantClass N N (Function.swap fun x x_1 => x + x_1) r] :

ContravariantClass N N (Function.swap fun x x_1 => x + x_1) r

Equations

@AddGroup.covconv_swap = @AddGroup.covconv_swap.proof_1

instance Group.covconv_swap {N : Type u_1} {r : N → N → Prop} [inst : Group N] [inst : CovariantClass N N (Function.swap fun x x_1 => x * x_1) r] :

ContravariantClass N N (Function.swap fun x x_1 => x * x_1) r

Equations

@Group.covconv_swap = @Group.covconv_swap.proof_1

theorem act_rel_of_rel_of_act_rel {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : CovariantClass M N μ r] [inst : 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} [inst : CovariantClass M N μ r] [inst : 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_1} {r : N → N → Prop} {mu : N → N → N} [inst : 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} [inst : 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} [inst : ContravariantClass M N μ r] [inst : 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} [inst : ContravariantClass M N μ r] [inst : 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} [inst : Preorder N] [inst : CovariantClass M N μ fun x x_1 => x ≤ x_1] (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} [inst : Preorder α] [inst : Preorder N] {f : N → α} [inst : CovariantClass M N μ fun x x_1 => x ≤ x_1] (hf : Monotone f) (m : M) :

Monotone fun n => f (μ m n)

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

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

Monotone fun n => f (μ n m)

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

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

Antitone fun n => f (μ m n)

Dual of Monotone.covariant_of_const

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

Antitone fun n => f (μ n m)

Dual of Monotone.covariant_of_const'

theorem covariant_le_of_covariant_lt (M : Type u_2) (N : Type u_1) (μ : M → N → N) [inst : PartialOrder N] :

(Covariant M N μ fun x x_1 => x < x_1) → Covariant M N μ fun x x_1 => x ≤ x_1

theorem contravariant_lt_of_contravariant_le (M : Type u_2) (N : Type u_1) (μ : 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

theorem covariant_le_iff_contravariant_lt (M : Type u_2) (N : Type u_1) (μ : 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

theorem covariant_lt_iff_contravariant_le (M : Type u_2) (N : Type u_1) (μ : 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

theorem flip_add (N : Type u_1) [inst : AddCommSemigroup N] :

(flip fun x x_1 => x + x_1) = fun x x_1 => x + x_1

theorem flip_mul (N : Type u_1) [inst : CommSemigroup N] :

(flip fun x x_1 => x * x_1) = fun x x_1 => x * x_1

theorem covariant_flip_add_iff (N : Type u_1) (r : N → N → Prop) [inst : AddCommSemigroup N] :

Covariant N N (flip fun x x_1 => x + x_1) r ↔ Covariant N N (fun x x_1 => x + x_1) r

theorem covariant_flip_mul_iff (N : Type u_1) (r : N → N → Prop) [inst : CommSemigroup N] :

Covariant N N (flip fun x x_1 => x * x_1) r ↔ Covariant N N (fun x x_1 => x * x_1) r

theorem contravariant_flip_add_iff (N : Type u_1) (r : N → N → Prop) [inst : AddCommSemigroup N] :

Contravariant N N (flip fun x x_1 => x + x_1) r ↔ Contravariant N N (fun x x_1 => x + x_1) r

theorem contravariant_flip_mul_iff (N : Type u_1) (r : N → N → Prop) [inst : CommSemigroup N] :

Contravariant N N (flip fun x x_1 => x * x_1) r ↔ Contravariant N N (fun x x_1 => x * x_1) r

instance contravariant_add_lt_of_covariant_add_le (N : Type u_1) [inst : Add N] [inst : LinearOrder N] [inst : CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :

ContravariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1

Equations

contravariant_add_lt_of_covariant_add_le = contravariant_add_lt_of_covariant_add_le.proof_1

def contravariant_add_lt_of_covariant_add_le.proof_1 (N : Type u_1) [inst : Add N] [inst : LinearOrder N] [inst : CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :

ContravariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1

Equations

(_ : ContravariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1) = (_ : ContravariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1)

instance contravariant_mul_lt_of_covariant_mul_le (N : Type u_1) [inst : Mul N] [inst : LinearOrder N] [inst : CovariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] :

ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1

Equations

contravariant_mul_lt_of_covariant_mul_le = contravariant_mul_lt_of_covariant_mul_le.proof_1

def covariant_add_lt_of_contravariant_add_le.proof_1 (N : Type u_1) [inst : Add N] [inst : LinearOrder N] [inst : ContravariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :

CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1

Equations

(_ : CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1) = (_ : CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1)

instance covariant_add_lt_of_contravariant_add_le (N : Type u_1) [inst : Add N] [inst : LinearOrder N] [inst : ContravariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :

CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1

Equations

covariant_add_lt_of_contravariant_add_le = covariant_add_lt_of_contravariant_add_le.proof_1

instance covariant_mul_lt_of_contravariant_mul_le (N : Type u_1) [inst : Mul N] [inst : LinearOrder N] [inst : ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] :

CovariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1

Equations

covariant_mul_lt_of_contravariant_mul_le = covariant_mul_lt_of_contravariant_mul_le.proof_1

instance covariant_swap_add_le_of_covariant_add_le (N : Type u_1) [inst : AddCommSemigroup N] [inst : LE N] [inst : CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :

CovariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

covariant_swap_add_le_of_covariant_add_le = covariant_swap_add_le_of_covariant_add_le.proof_1

def covariant_swap_add_le_of_covariant_add_le.proof_1 (N : Type u_1) [inst : AddCommSemigroup N] [inst : LE N] [inst : CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :

CovariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

(_ : CovariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1) = (_ : CovariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1)

instance covariant_swap_mul_le_of_covariant_mul_le (N : Type u_1) [inst : CommSemigroup N] [inst : LE N] [inst : CovariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] :

CovariantClass N N (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

Equations

covariant_swap_mul_le_of_covariant_mul_le = covariant_swap_mul_le_of_covariant_mul_le.proof_1

def contravariant_swap_add_le_of_contravariant_add_le.proof_1 (N : Type u_1) [inst : AddCommSemigroup N] [inst : LE N] [inst : ContravariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :

ContravariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

(_ : ContravariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1) = (_ : ContravariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1)

instance contravariant_swap_add_le_of_contravariant_add_le (N : Type u_1) [inst : AddCommSemigroup N] [inst : LE N] [inst : ContravariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :

ContravariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

contravariant_swap_add_le_of_contravariant_add_le = contravariant_swap_add_le_of_contravariant_add_le.proof_1

instance contravariant_swap_mul_le_of_contravariant_mul_le (N : Type u_1) [inst : CommSemigroup N] [inst : LE N] [inst : ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] :

ContravariantClass N N (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

Equations

contravariant_swap_mul_le_of_contravariant_mul_le = contravariant_swap_mul_le_of_contravariant_mul_le.proof_1

instance contravariant_swap_add_lt_of_contravariant_add_lt (N : Type u_1) [inst : AddCommSemigroup N] [inst : LT N] [inst : ContravariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :

ContravariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1

Equations

contravariant_swap_add_lt_of_contravariant_add_lt = contravariant_swap_add_lt_of_contravariant_add_lt.proof_1

def contravariant_swap_add_lt_of_contravariant_add_lt.proof_1 (N : Type u_1) [inst : AddCommSemigroup N] [inst : LT N] [inst : ContravariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :

ContravariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1

Equations

(_ : ContravariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1) = (_ : ContravariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1)

instance contravariant_swap_mul_lt_of_contravariant_mul_lt (N : Type u_1) [inst : CommSemigroup N] [inst : LT N] [inst : ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1] :

ContravariantClass N N (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1

Equations

contravariant_swap_mul_lt_of_contravariant_mul_lt = contravariant_swap_mul_lt_of_contravariant_mul_lt.proof_1

def covariant_swap_add_lt_of_covariant_add_lt.proof_1 (N : Type u_1) [inst : AddCommSemigroup N] [inst : LT N] [inst : CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :

CovariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1

Equations

(_ : CovariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1) = (_ : CovariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1)

instance covariant_swap_add_lt_of_covariant_add_lt (N : Type u_1) [inst : AddCommSemigroup N] [inst : LT N] [inst : CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :

CovariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1

Equations

covariant_swap_add_lt_of_covariant_add_lt = covariant_swap_add_lt_of_covariant_add_lt.proof_1

instance covariant_swap_mul_lt_of_covariant_mul_lt (N : Type u_1) [inst : CommSemigroup N] [inst : LT N] [inst : CovariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1] :

CovariantClass N N (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1

Equations

covariant_swap_mul_lt_of_covariant_mul_lt = covariant_swap_mul_lt_of_covariant_mul_lt.proof_1

instance AddLeftCancelSemigroup.covariant_add_lt_of_covariant_add_le (N : Type u_1) [inst : AddLeftCancelSemigroup N] [inst : PartialOrder N] [inst : CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :

CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1

Equations

AddLeftCancelSemigroup.covariant_add_lt_of_covariant_add_le = AddLeftCancelSemigroup.covariant_add_lt_of_covariant_add_le.proof_1

def AddLeftCancelSemigroup.covariant_add_lt_of_covariant_add_le.proof_1 (N : Type u_1) [inst : AddLeftCancelSemigroup N] [inst : PartialOrder N] [inst : CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :

CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1

Equations

(_ : CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1) = (_ : CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1)

instance LeftCancelSemigroup.covariant_mul_lt_of_covariant_mul_le (N : Type u_1) [inst : LeftCancelSemigroup N] [inst : PartialOrder N] [inst : CovariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] :

CovariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1

Equations

LeftCancelSemigroup.covariant_mul_lt_of_covariant_mul_le = LeftCancelSemigroup.covariant_mul_lt_of_covariant_mul_le.proof_1

instance AddRightCancelSemigroup.covariant_swap_add_lt_of_covariant_swap_add_le (N : Type u_1) [inst : AddRightCancelSemigroup N] [inst : PartialOrder N] [inst : CovariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :

CovariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1

Equations

AddRightCancelSemigroup.covariant_swap_add_lt_of_covariant_swap_add_le = AddRightCancelSemigroup.covariant_swap_add_lt_of_covariant_swap_add_le.proof_1

def AddRightCancelSemigroup.covariant_swap_add_lt_of_covariant_swap_add_le.proof_1 (N : Type u_1) [inst : AddRightCancelSemigroup N] [inst : PartialOrder N] [inst : CovariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :

CovariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1

Equations

(_ : CovariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1) = (_ : CovariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1)

instance RightCancelSemigroup.covariant_swap_mul_lt_of_covariant_swap_mul_le (N : Type u_1) [inst : RightCancelSemigroup N] [inst : PartialOrder N] [inst : CovariantClass N N (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] :

CovariantClass N N (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1

Equations

RightCancelSemigroup.covariant_swap_mul_lt_of_covariant_swap_mul_le = RightCancelSemigroup.covariant_swap_mul_lt_of_covariant_swap_mul_le.proof_1

instance AddLeftCancelSemigroup.contravariant_add_le_of_contravariant_add_lt (N : Type u_1) [inst : AddLeftCancelSemigroup N] [inst : PartialOrder N] [inst : ContravariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :

ContravariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

AddLeftCancelSemigroup.contravariant_add_le_of_contravariant_add_lt = AddLeftCancelSemigroup.contravariant_add_le_of_contravariant_add_lt.proof_1

def AddLeftCancelSemigroup.contravariant_add_le_of_contravariant_add_lt.proof_1 (N : Type u_1) [inst : AddLeftCancelSemigroup N] [inst : PartialOrder N] [inst : ContravariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :

ContravariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

(_ : ContravariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1) = (_ : ContravariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1)

instance LeftCancelSemigroup.contravariant_mul_le_of_contravariant_mul_lt (N : Type u_1) [inst : LeftCancelSemigroup N] [inst : PartialOrder N] [inst : ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1] :

ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

Equations

LeftCancelSemigroup.contravariant_mul_le_of_contravariant_mul_lt = LeftCancelSemigroup.contravariant_mul_le_of_contravariant_mul_lt.proof_1

instance AddRightCancelSemigroup.contravariant_swap_add_le_of_contravariant_swap_add_lt (N : Type u_1) [inst : AddRightCancelSemigroup N] [inst : PartialOrder N] [inst : ContravariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] :

ContravariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

AddRightCancelSemigroup.contravariant_swap_add_le_of_contravariant_swap_add_lt = AddRightCancelSemigroup.contravariant_swap_add_le_of_contravariant_swap_add_lt.proof_1

def AddRightCancelSemigroup.contravariant_swap_add_le_of_contravariant_swap_add_lt.proof_1 (N : Type u_1) [inst : AddRightCancelSemigroup N] [inst : PartialOrder N] [inst : ContravariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] :

ContravariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

(_ : ContravariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1) = (_ : ContravariantClass N N (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1)

instance RightCancelSemigroup.contravariant_swap_mul_le_of_contravariant_swap_mul_lt (N : Type u_1) [inst : RightCancelSemigroup N] [inst : PartialOrder N] [inst : ContravariantClass N N (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] :

ContravariantClass N N (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

Equations

RightCancelSemigroup.contravariant_swap_mul_le_of_contravariant_swap_mul_lt = RightCancelSemigroup.contravariant_swap_mul_le_of_contravariant_swap_mul_lt.proof_1