image — Mathlib

English

Under a restriction, the image of quasispectrum R a under algebraMap R S equals quasispectrum S a.

Русский

При ограничении изображение quasispectrum R a под алгебраMap равно quasispectrum S a.

LaTeX

$$$\\mathrm{QuasispectrumRestricts}(a,f) \\Rightarrow \\mathrm{Set.image}(\\mathrm{algebraMap}_{R,S}, \\mathrm{quasispectrum}(R,a)) = \\mathrm{quasispectrum}(S,a)$$$

Lean4

theorem image (h : QuasispectrumRestricts a f) : f '' quasispectrum S a = quasispectrum R a := by
  simp only [← h.algebraMap_image, Set.image_image, h.left_inv _, Set.image_id']

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