English
If SpectrumRestricts a f, then the image equality holds: Set.image(algebraMap R S)(spectrum R a) = spectrum S a.
Русский
Если SpectrumRestricts a f, то выполняется равенство образов: Set.image(algebraMap R S)(spectrum R a) = spectrum S a.
LaTeX
$$$ \\mathrm{Set.image}(\\mathrm{algebraMap} R S)(\\mathrm{spectrum} R a) = \\mathrm{spectrum} S a $$$
Lean4
theorem image (h : SpectrumRestricts a f) : f '' spectrum S a = spectrum R a := by
simp only [← h.algebraMap_image, Set.image_image, h.left_inv _, Set.image_id']