cancel_right — Mathlib

English

If f is surjective and g1 ∘ f = g2 ∘ f, then g1 = g2.

Русский

Пусть f: α →_{CO} β сюръективно. Тогда из g1 ∘ f = g2 ∘ f следует g1 = g2.

LaTeX

$$$$ \forall f:\alpha \to_{CO} \beta,\; \forall g_1,g_2:\beta \to_{CO} \gamma,\; \mathrm{Surjective}(f) \Rightarrow (g_1 \circ f = g_2 \circ f \iff g_1 = g_2). $$$$

Lean4

@[simp]
theorem cancel_right {g₁ g₂ : β →CO γ} {f : α →CO β} (hf : Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, fun h => congr_arg₂ _ h rfl⟩

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