cancel_left — Mathlib

English

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

Русский

Если f инъективен, то f ∘ g1 = f ∘ g2 подразумевает g1 = g2.

LaTeX

$$$\text{Injective } f \Rightarrow (f \circ g_1 = f \circ g_2 \;\iff\; g_1 = g_2)$$$

Lean4

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

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