rightInvOn — Mathlib

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 _ _

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