summand_smul_def — Mathlib

English

Under suitable hypotheses, all maps into the pushout are injective; in particular, each of the base injections of G i into PushoutI is injective when the corresponding φ i are injective.

Русский

При соответствующих предпосылках все отображения в пушаут инъективны; в частности, каждое вхождение G_i в PushoutI инъективно, если соответствующее φ_i инъективно.

LaTeX

$$$$\text{If } (\forall i, \; φ_i : H \to G_i) \text{ is injective, then } (\forall i, of(i) : G_i \to PushoutI(φ) \text{ is injective}).$$$$

Lean4

theorem summand_smul_def {i : ι} (g : G i) (w : NormalWord d) :
    of (φ := φ) i g • w = (equivPair i).symm { equivPair i w with head := g * (equivPair i w).head } :=
  rfl

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