of_subset_range_algebraMap — Mathlib

English

If f has a left inverse of the algebra map R → S and quasispectrum S a lies in the range of algebraMap, then QuasispectrumRestricts a f.

Русский

Если у f есть левосторонний обратный к алгебраическому отображению R → S и quasispectrum S a лежит в диапазоне algebraMap, то QuasispectrumRestricts a f.

LaTeX

$$$\\text{LeftInverse}(f, \\text{algebraMap}) \\land \\mathrm{quasispectrum}(S,a) \\subseteq \\mathrm{range}(\\text{algebraMap}) \\Rightarrow \\mathrm{QuasispectrumRestricts}(a,f)$$$

Lean4

theorem of_subset_range_algebraMap (hf : f.LeftInverse (algebraMap R S))
    (h : quasispectrum S a ⊆ Set.range (algebraMap R S)) : QuasispectrumRestricts a f
    where
  rightInvOn := fun s hs => by obtain ⟨r, rfl⟩ := h hs; rw [hf r]
  left_inv := hf

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