act_rel_act_of_rel — Mathlib

English

If CovariantClass M N μ r holds, then applying μ to both arguments preserves the relation: if r a b then r (μ m a) (μ m b).

Русский

Если CovariantClass M N μ r выполняется, то применение μ к обоим аргументам сохраняет отношение: если r a b, тогда r(μ m a, μ m b).

LaTeX

$$∀ m ∈ M, {a,b ∈ N}, r a b → r (μ m a) (μ m b)$$

Lean4

theorem act_rel_act_of_rel (m : M) {a b : N} (ab : r a b) : r (μ m a) (μ m b) :=
  CovariantClass.elim _ ab

Похожие утверждения