quasispectrumRestricts_iff — Mathlib

English

If hf is a left inverse of algebraMap R S and quasispectrum S a ⊆ range (algebraMap R S), then a QuasispectrumRestricts a f holds.

Русский

Если hf — левый обратный к algebraMap R S и quasispectrum S a ⊆ range (algebraMap R S), то выполняется QuasispectrumRestricts a f.

LaTeX

$$QuasispectrumRestricts a f$$

Lean4

theorem quasispectrumRestricts_iff {R S A : Type*} [CommSemiring R] [CommSemiring S] [NonUnitalRing A] [Module R A]
    [Module S A] [Algebra R S] (a : A) (f : S → R) :
    QuasispectrumRestricts a f ↔
      (quasispectrum S a).RightInvOn f (algebraMap R S) ∧ Function.LeftInverse f (algebraMap R S) :=
  ⟨fun ⟨h₁, h₂⟩ ↦ ⟨h₁, h₂⟩, fun ⟨h₁, h₂⟩ ↦ ⟨h₁, h₂⟩⟩

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