of_quasispectrum_eq — Mathlib

English

If a is restricted by f to R and the quasispectrum of S a equals that of S b, then b with the same f is also restricted.

Русский

Если спектр квази-спектра a ограничен через f, и quasispectrum S a = quasispectrum S b, то ограничение распространяется на b.

LaTeX

$$$\\mathrm{QuasispectrumRestricts}(a,f) \\land (\\mathrm{quasispectrum}(S,a) = \\mathrm{quasispectrum}(S,b)) \\Rightarrow \\mathrm{QuasispectrumRestricts}(b,f)$$$

Lean4

theorem of_quasispectrum_eq {a b : A} {f : S → R} (ha : QuasispectrumRestricts a f)
    (h : quasispectrum S a = quasispectrum S b) : QuasispectrumRestricts b f
    where
  rightInvOn := h ▸ ha.rightInvOn
  left_inv := ha.left_inv

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