exists_mem_support_pos_pairingIn_ne_zero

English

If i is positive, there exists a finite sum decomposition of P.root i as a sum of roots of elements from the base support with a universal partial-sum property.

Русский

Если i положительно, существует конечная сумма корней P.root i как сумма корней элементов из опоры основы со свойством частичных сумм.

LaTeX

$$b.IsPos i → ∃ n, ∃ f : Fin n → ι, range f ⊆ b.support ∧ P.root i = ∑ m, P.root (f m) ∧ ∀ m, ∑ m' ≤ m, P.root (f m') ∈ range P.root$$

Lean4

theorem exists_mem_support_pos_pairingIn_ne_zero [P.IsCrystallographic] (i : ι) :
    ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0 :=
  by
  rcases IsPos.or_neg b i with hi | hi
  · obtain ⟨j, hj, hj₀⟩ := hi.exists_mem_support_pos_pairingIn
    exact ⟨j, hj, hj₀.ne'⟩
  · obtain ⟨j, hj, hj₀⟩ := hi.exists_mem_support_pos_pairingIn
    exact ⟨j, hj, by aesop⟩

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