Theorems · Theorem · order theory

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

Defined in

Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Cited by

6 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CovariantClassContravariantClass