cancel_left — Mathlib

English

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

Русский

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

LaTeX

$$$\\forall g_1,g_2:\\mathrm{BoundedLatticeHom}(\\beta,\\gamma),\\ f:\\mathrm{BoundedLatticeHom}(\\alpha,\\beta),\\ hf: \\text{Surjective} \\ f\\Rightarrow (g_1\\circ f = g_2\\circ f) \\Leftrightarrow g_1 = g_2$$$

Lean4

@[simp]
theorem cancel_left {g : BoundedLatticeHom β γ} {f₁ f₂ : BoundedLatticeHom α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

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