cancel_right — Mathlib

English

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

Русский

Если g1 ∘ f = g2 ∘ f и f сюръктивно отображает, то g1 = g2; наоборот, если g1 = g2, то g1 ∘ f = g2 ∘ f.

LaTeX

$$$\\forall g_1,g_2 : \\operatorname{LocallyBoundedMap} \\beta \\gamma, \\forall f : \\operatorname{LocallyBoundedMap} \\alpha \\beta, \\text{hf} : \\operatorname{Surjective} (\\operatorname{coe} f), (g_1 \\circ f) = (g_2 \\circ f) \\iff g_1 = g_2.$$$

Lean4

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

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