disjoint_iInf_maxGenEigenspace — Mathlib

English

If χ1 ≠ χ2, the iInf of their maxGenEigenspace are disjoint.

Русский

Если χ1 не равно χ2, то их iInf-обобщённые собственные пространства взаимоисключаются.

LaTeX

$$$$ \operatorname{Disjoint}\left(\inf_i (f_i).maxGenEigenspace(χ_1(i)), \inf_i (f_i).maxGenEigenspace(χ_2(i))\right). $$$$

Lean4

theorem disjoint_iInf_maxGenEigenspace {χ₁ χ₂ : ι → R} (h : χ₁ ≠ χ₂) :
    Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (⨅ i, (f i).maxGenEigenspace (χ₂ i)) :=
  by
  obtain ⟨j, hj⟩ : ∃ j, χ₁ j ≠ χ₂ j := Function.ne_iff.mp h
  exact (End.disjoint_genEigenspace (f j) hj ⊤ ⊤).mono (iInf_le _ j) (iInf_le _ j)

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