comp_left_injective — Mathlib

English

As above, left-injectivity holds for the composition with e.

Русский

Как выше, левая инъективность сохраняется при композиции с e.

LaTeX

$$$$ \text{Injective } (f \mapsto (e : M \to^* N).comp f). $$$$

Lean4

@[to_additive]
theorem comp_left_injective (e : M ≃* N) : Injective fun f : N →* P ↦ f.comp (e : M →* N) :=
  LeftInverse.injective (g := fun f ↦ f.comp e.symm) fun f ↦ by simp [MonoidHom.comp_assoc]

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