Theorems · Theorem · order theory

ContravariantClass.elim

∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [self : ContravariantClass M N μ r],
  Contravariant M N μ r

For all m ∈ M and all elements 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₂).

Defined in

Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Cited by

12 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

ContravariantClass