cancel_right — Mathlib

English

If f is surjective, then right composition with f is injective on BiheytingHom β γ: for g1,g2, g1 ∘ f = g2 ∘ f implies g1 = g2.

Русский

Если f сюръективно отображает, то правое композиционное отображение на BiheytingHom β γ инъективно: 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

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

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