cancel_left — Mathlib

English

Let g be an injective spectral map β → γ and f1, f2 be spectral maps α → β. Then g ∘ f1 = g ∘ f2 if and only if f1 = f2.

Русский

Пусть g — инъективное спектральное отображение β → γ, а f1, f2 — спектральные отображения α → β. Тогда 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 : SpectralMap β γ} {f₁ f₂ : SpectralMap α β} (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 _⟩

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