English
If SpectrumRestricts a f, then f acts as a right inverse to the canonical algebra map on the spectrum of a; i.e., for every x in spectrum S a, (algebraMap R S)(f(x)) = x.
Русский
Если SpectrumRestricts a f, то f является правой инверсией к канонической алгебраической карте на спектре a; то есть для каждого x ∈ спектра S a выполняется (algebraMap R S)(f(x)) = x.
LaTeX
$$$ SpectrumRestricts(a,f) \\rightarrow (spectrum S a).RightInvOn f (algebraMap R S) $$$
Lean4
theorem rightInvOn (h : SpectrumRestricts a f) : (spectrum S a).RightInvOn f (algebraMap R S) :=
(QuasispectrumRestricts.rightInvOn h).mono <| spectrum_subset_quasispectrum _ _