right_cancellable — Mathlib

English

If f: α → β is surjective, then for any g1,g2: β → γ, equality g1 ∘ f = g2 ∘ f implies g1 = g2.

Русский

Если f: α → β сюръективен, то для любых g1,g2: β → γ, равенство g1 ∘ f = g2 ∘ f требует, чтобы g1 = g2.

LaTeX

$$$\operatorname{Surjective}(f) \Rightarrow (\forall g_1,g_2:β \to γ,\ g_1 \circ f = g_2 \circ f \iff g_1 = g_2).$$$

Lean4

protected theorem right_cancellable (hf : Surjective f) {g₁ g₂ : β → γ} : g₁ ∘ f = g₂ ∘ f ↔ g₁ = g₂ :=
  hf.injective_comp_right.eq_iff

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