cancel_right — Mathlib

English

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

Русский

Если f сюръективен, то для BiheytingHom выполняется: g1 ∘ f = g2 ∘ f ⇔ g1 = g2.

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_right (hf : Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, congr_arg (fun a ↦ comp a f)⟩

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