injOn_iInf_maxGenEigenspace — Mathlib

English

The map χ ↦ iInf_i (f_i).maxGenEigenspace(χ_i) is injective on nonzero values.

Русский

Отображение χ ↦ iInf_i maxGenEigenspace(χ_i) инъективно на непустых значениях.

LaTeX

$$$$ \operatorname{InjOn}\left(\lambda \chi.\; \inf_i (f_i).maxGenEigenspace(\chi_i)\right)\; \{\chi\;|\; \inf_i (f_i).maxGenEigenspace(\chi_i) \neq 0\} $$$$

Lean4

theorem injOn_iInf_maxGenEigenspace :
    InjOn (fun χ : ι → R ↦ ⨅ i, (f i).maxGenEigenspace (χ i)) {χ | ⨅ i, (f i).maxGenEigenspace (χ i) ≠ ⊥} :=
  by
  rintro χ₁ _ χ₂ hχ₂ (hχ₁₂ : ⨅ i, (f i).maxGenEigenspace (χ₁ i) = ⨅ i, (f i).maxGenEigenspace (χ₂ i))
  contrapose! hχ₂
  simpa [hχ₁₂] using disjoint_iInf_maxGenEigenspace f hχ₂

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