cancel_left — Mathlib

English

If f is surjective, then g1 ∘ f = g2 ∘ f iff g1 = g2 for BiheytingHom.

Русский

Если f сюръективен, то g1 ∘ f = g2 ∘ f тогда и только тогда, когда g1 = g2 для BiheytingHom.

LaTeX

$$$\forall f:\mathrm{BiheytingHom}(\alpha,\beta),\ (\mathrm{Surjective}(f))\to( g_1\circ f = g_2\circ f \iff g_1 = g_2 )$$$

Lean4

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

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