cancel_left — Mathlib

English

If g is injective, then left cancellation holds: 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 : sInfHom β γ} {f₁ f₂ : sInfHom α β} (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 _⟩

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