cancel_left — Mathlib

English

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

Русский

Если f ∘ g1 = f ∘ g2 и f инъективен, то g1 = g2.

LaTeX

$$$(f \circ g_1 = f \circ g_2) \;\Rightarrow\; g_1 = g_2 \quad\text{provided } \mathrm{Injective}(f)$$$

Lean4

@[simp]
theorem cancel_left {f : β →+*o γ} {g₁ g₂ : α →+*o β} (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 _⟩

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