Theorems · Theorem · order theory

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

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

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

Function.swapstatement and proof · cited by 216
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 by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.