coxeterWeightIn_mem_set_of_isCrystallographic

English

If P is crystallographic, then coxeterWeightIn ℤ i j ∈ {0,1,2,3,4}.

Русский

Если P кристаллографична, то coxeterWeightIn ℤ i j ∈ {0,1,2,3,4}.

LaTeX

$$P.coxeterWeightIn ℤ i j ∈ \{0,1,2,3,4\}$$

Lean4

theorem coxeterWeightIn_mem_set_of_isCrystallographic : P.coxeterWeightIn ℤ i j ∈ ({0, 1, 2, 3, 4} : Set ℤ) :=
  by
  have : Fintype ι := Fintype.ofFinite ι
  obtain ⟨n, hcn⟩ : ∃ n : ℕ, P.coxeterWeightIn ℤ i j = n :=
    by
    have : 0 ≤ P.coxeterWeightIn ℤ i j := by
      simpa only [P.algebraMap_coxeterWeightIn] using P.coxeterWeight_nonneg (P.posRootForm ℤ) i j
    obtain ⟨n, hn⟩ := Int.eq_ofNat_of_zero_le this
    exact ⟨n, by simp [hn]⟩
  have : P.coxeterWeightIn ℤ i j ≤ 4 := P.coxeterWeightIn_le_four ℤ i j
  simp only [hcn, mem_insert_iff, mem_singleton_iff] at this ⊢
  norm_cast at this ⊢
  cutsat

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