cancel_left — Mathlib

English

If g is injective, then g ∘ f1 = g ∘ f2 implies f1 = f2.

Русский

Пусть g: β →_{CO} γ инъективно. Тогда g ∘ f1 = g ∘ f2 → f1 = f2.

LaTeX

$$$$ \forall g:\beta \to_{CO} \gamma,\; \forall f_1,f_2:\alpha \to_{CO} \beta,\; \mathrm{Injective}(g) \Rightarrow (g \circ f_1 = g \circ 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 _⟩

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