of_spectrum_eq — Mathlib

English

If f is left-inverse to algebraMap R S and spectrum S a is contained in the range of algebraMap R S, then SpectrumRestricts a f.

Русский

Если f является левой инверсией к algebraMap R S и spectrum S a ⊆ range(algebraMap R S), тогда SpectrumRestricts a f.

LaTeX

$$$ (f\\LeftInverse (\\mathrm{algebraMap } R S)) \\land (\\mathrm{spectrum} S a \\subseteq \\mathrm{range}(\\mathrm{algebraMap } R S)) \\rightarrow \\mathrm{SpectrumRestricts } a f $$$

Lean4

theorem of_spectrum_eq {a b : A} {f : S → R} (ha : SpectrumRestricts a f) (h : spectrum S a = spectrum S b) :
    SpectrumRestricts b f
    where
  rightInvOn := by
    rw [quasispectrum_eq_spectrum_union_zero, ← h, ← quasispectrum_eq_spectrum_union_zero]
    exact QuasispectrumRestricts.rightInvOn ha
  left_inv := ha.left_inv

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