algebraMap_image — Mathlib

English

If h is QuasispectrumRestricts a f, then the image of quasispectrum S a under f equals quasispectrum R a.

Русский

Если h — ограничение квазиспеktrа, то образ quasispectrum S a под действием f равен quasispectrum R a.

LaTeX

$$$\\mathrm{QuasispectrumRestricts}(a,f) \\Rightarrow f''\\mathrm{quasispectrum}(S,a) = \\mathrm{quasispectrum}(R,a)$$$

Lean4

theorem algebraMap_image (h : QuasispectrumRestricts a f) : algebraMap R S '' quasispectrum R a = quasispectrum S a :=
  by
  refine Set.eq_of_subset_of_subset ?_ fun s hs => ⟨f s, ?_⟩
  · simpa only [quasispectrum.preimage_algebraMap] using (quasispectrum S a).image_preimage_subset (algebraMap R S)
  exact ⟨quasispectrum.of_algebraMap_mem S ((h.rightInvOn hs).symm ▸ hs), h.rightInvOn hs⟩

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