cancel_left — Mathlib

English

If g is injective, then composing on the left with g is injective: g ∘ f1 = g ∘ f2 implies f1 = f2.

Русский

Если g инъективно, то левое сокращение сохраняет равенство функций: g ∘ f1 = g ∘ f2 ⇒ f1 = f2.

LaTeX

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

Lean4

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

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