subset_preimage — Mathlib

English

If h is QuasispectrumRestricts a f, then quasispectrum S a is contained in the preimage of quasispectrum R a under f.

Русский

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

LaTeX

$$$\\mathrm{quasispectrum}(S,a) \\subseteq f^{-1}\\bigl(\\mathrm{quasispectrum}(R,a)\\bigr)$$$

Lean4

theorem subset_preimage (h : QuasispectrumRestricts a f) : quasispectrum S a ⊆ f ⁻¹' quasispectrum R a :=
  h.image ▸ (quasispectrum S a).subset_preimage_image f

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