cancel_right — Mathlib

English

If f is surjective and g1∘f = g2∘f, then g1 = g2; conversely, equality of g1 and g2 implies equality after composing with f.

Русский

Если f сюръективное и g1∘f = g2∘f, то g1 = g2; наоборот, равенство g1 и g2 следует из их композиции с f.

LaTeX

$$$\big(g_1\circ f = g_2\circ f\big) \iff g_1 = g_2\quad \text{(for surjective } f\text{)}$$$

Lean4

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

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