Theorems · Theorem · order theory

CovariantClass.elim

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

For all m ∈ M and all elements n₁, n₂ ∈ N, if the relation r holds for the pair (n₁, n₂), then, the relation r also holds for the pair (μ m n₁, μ m n₂)

Defined in

Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Cited by

22 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

CovariantClass