cancel_right — Mathlib

English

If f is surjective, then precomposing by f is right-cancelable: g1 ∘ f = g2 ∘ f implies g1 = g2.

Русский

Если f сюръективен, то правое умножение на f отменяется: g1 ∘ f = g2 ∘ f ⇒ g1 = g2.

LaTeX

$$g1.comp f = g2.comp f ⇔ g1 = g2, with hf : Surjective f$$

Lean4

@[simp]
theorem cancel_right {g₁ g₂ f : CentroidHom α} (hf : Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h ↦ ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, fun a ↦ congrFun (congrArg comp a) f⟩

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