cancel_right — Mathlib

English

If f is surjective, then precomposition by f is injective on spectral maps: g1 ∘ f = g2 ∘ f implies g1 = g2.

Русский

Если f сюръективно, то предобраз по f инъективен на спектральных отображениях: g1 ∘ f = g2 ∘ f ⇒ g1 = g2.

LaTeX

$$$ \text{Surjective}(f) \Rightarrow (g_1.comp f = g_2.comp f) \iff g_1 = g_2. $$$

Lean4

@[simp]
theorem cancel_right {g₁ g₂ : SpectralMap β γ} {f : SpectralMap α β} (hf : Surjective f) :
    g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, fun a => of_eq (congrFun (congrArg comp a) f)⟩

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