cancel_right — Mathlib

English

If f is surjective, then composing on the right with f is injective on morphisms: g1 ∘ f = g2 ∘ f iff g1 = g2.

Русский

Пусть f суръективно отображает, тогда композиция справа с f инъективна; т.е. g1 ∘ f = g2 ∘ f тогда и только тогда, когда g1 = g2.

LaTeX

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

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)⟩

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