genWeightSpaceChain_def' — Mathlib

English

GenWeightSpaceChain equals WeightSpaceChain under relabeling with prime (Def'): genWeightSpaceChain M χ1 χ2 p q = ⨆ k ∈ Finset.Ioo(p,q), genWeightSpace M (k • χ1 + χ2).

Русский

GenWeightSpaceChain равна WeightSpaceChain при ограничении до Finset.Ioo; def' версии: genWeightSpaceChain M χ1 χ2 p q = ⨆ k ∈ Finset.Ioo(p,q), genWeightSpace M (k • χ1 + χ2).

LaTeX

$$$\text{genWeightSpaceChain}(M, χ_1, χ_2, p, q) = \displaystyle \big\langle k \in Finset.Ioo(p,q) \mapsto genWeightSpace(M, k \cdot χ_1 + χ_2) \big\rangle$$$

Lean4

theorem genWeightSpaceChain_def' :
    genWeightSpaceChain M χ₁ χ₂ p q = ⨆ k ∈ Finset.Ioo p q, genWeightSpace M (k • χ₁ + χ₂) :=
  by
  have : ∀ (k : ℤ), k ∈ Ioo p q ↔ k ∈ Finset.Ioo p q := by simp
  simp_rw [genWeightSpaceChain_def, this]

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