act_rel_of_rel_of_act_rel — Mathlib

English

Let μ be an action of M on N compatible with the relation r. If a is related to b and μ(m,b) is related to c, then μ(m,a) is related to c.

Русский

Пусть μ — действие M на N, совместимое с отношением r. Если a связано с b, и μ(m,b) связано с c, тогда μ(m,a) связано с c.

LaTeX

$$$\forall m\in M\,\forall a,b,c\in N,\ r(a,b) \to r(\mu\,m\,b,c) \to r(\mu\,m\,a,c)$$$

Lean4

theorem act_rel_of_rel_of_act_rel (ab : r a b) (rl : r (μ m b) c) : r (μ m a) c :=
  _root_.trans (act_rel_act_of_rel m ab) rl

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