Theorems · Theorem · order theory

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

Defined in: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Cited by: 0 results in Mathlib
Foundations: Depth 3 from the axioms · uses no axioms
Assumes: ContravariantClass 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
ContravariantClassstatement and proof · cited by 15
rel_of_act_rel_actproof · cited by 2

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.