cancel_right — Mathlib

English

If f is surjective, then right cancellation holds for sInfHom: g1 ∘ f = g2 ∘ f implies g1 = g2; and conversely.

Русский

Если f сюръективна, то правое сокращение для sInfHom: g1 ∘ f = g2 ∘ f ⇒ g1 = g2; обратно следует, если g1 = g2, то g1 ∘ f = g2 ∘ f.

LaTeX

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

Lean4

@[simp]
theorem cancel_right {g₁ g₂ : sInfHom β γ} {f : sInfHom α β} (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)⟩

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