cancel_right — Mathlib

English

If f is surjective, then g1 ∘ f = g2 ∘ f implies g1 = g2; equivalently, right-cancelation holds for surjective f.

Русский

Если f сюръективен, то g1 ∘ f = g2 ∘ f следовательно g1 = g2; правая отмена для сюръективного отображения.

LaTeX

$$$\\text{Surjective}(f) \\Rightarrow (g_1 \\circ f = g_2 \\circ f \\iff g_1 = g_2)$$$

Lean4

@[to_additive]
theorem cancel_right [One M] [One N] [One P] {g₁ g₂ : OneHom N P} {f : OneHom M N} (hf : Function.Surjective f) :
    g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => OneHom.ext <| hf.forall.2 (DFunLike.ext_iff.1 h), fun h => h ▸ rfl⟩

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