cancel_left — Mathlib

English

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

Русский

Если g инъективен и g∘f1 = g∘f2, тогда f1 = f2.

LaTeX

$$$\big(g\circ f_1 = g\circ f_2\big) \Rightarrow f_1=f_2\quad\text{(if }g\text{ injective)}$$$

Lean4

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

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