English
SpectrumRestricts a f is equivalent to having both a right-inverse on the spectrum and a left-inverse for algebraMap R S; i.e., SpectrumRestricts a f ⇔ (spectrum S a).RightInvOn f (algebraMap R S) ∧ LeftInverse f (algebraMap R S).
Русский
SpectrumRestricts a f эквивалентно тому, что на спектре имеет правая инверсия и левая инверсия относительно algebraMap R S; то есть SpectrumRestricts a f ⇔ (spectrum S a).RightInvOn f (algebraMap R S) ∧ LeftInverse f (algebraMap R S).
LaTeX
$$$ SpectrumRestricts(a,f) \\iff \\big( (spectrum S a).RightInvOn f (algebraMap R S) \\wedge \\mathrm{LeftInverse} f (\\mathrm{algebraMap } R S) \\big) $$$
Lean4
theorem _root_.spectrumRestricts_iff :
SpectrumRestricts a f ↔ (spectrum S a).RightInvOn f (algebraMap R S) ∧ Function.LeftInverse f (algebraMap R S) :=
⟨fun h ↦ ⟨h.rightInvOn, h.left_inv⟩, fun h ↦ .of_rightInvOn h.2 h.1⟩
