cancel_left — Mathlib

English

If g is injective, then g ∘ f1 = g ∘ f2 iff f1 = f2 for BiheytingHom.

Русский

Если g инъективен, то g ∘ f1 = g ∘ f2 эквивалентно f1 = f2 для BiheytingHom.

LaTeX

$$$\forall f_1,f_2:\mathrm{BiheytingHom}(\alpha,\beta),\ g:\mathrm{BiheytingHom}(\beta,\gamma),\ (\mathrm{Injective}(g))\to( g\circ f_1 = g\circ f_2 \iff f_1 = f_2 )$$$

Lean4

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

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