cancel_left — Mathlib

English

If g is injective, then g.comp f1 = g.comp f2 implies f1 = f2; and conversely, equality of f1 and f2 implies equality of their compositions with g.

Русский

Если g инъективно отображает, то g ∘ f1 = g ∘ f2 следуют f1 = f2; обратно равенство f1 = f2 приводит к равенству композиции.

LaTeX

$$$\text{Injective } g \Rightarrow (g.comp f_1 = g.comp f_2 \iff f_1 = f_2)$$$

Lean4

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

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