cancel_right — Mathlib

English

If g1 ∘ f = g2 ∘ f and f is surjective, then g1 = g2; i.e., post-composition with a surjective map is injective.

Русский

Если g1 ∘ f = g2 ∘ f и f сюръективно, тогда g1 = g2; пост-композиция с сюръективной картой инъективна.

LaTeX

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

Lean4

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

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