Theorems · Theorem · order theory

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 b c : N}, r a b → r (μ m b) c → r (μ m a) c

Defined in: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Cited by: 2 results in Mathlib
Foundations: Depth 3 from the axioms · uses no axioms
Assumes: CovariantClass IsTrans

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

IsTransstatement and proof · cited by 157
transproof · cited by 111
CovariantClassstatement and proof · cited by 25
act_rel_act_of_relproof · cited by 3

Cited by2

Results whose statement or proof uses this declaration.

mul_le_of_mul_le_leftproof · cited by 0
add_le_of_add_le_leftproof · cited by 0