zero_le_pairingIn_of_root_sub_mem

English

For i,j in a crystallographic, reduced, irreducible RootPairing with IsValuedIn, the sign of lt relation ensures pairingIn i j ≤ 0 implies pairingIn j i ≤ 0 and vice versa.

Русский

Для i,j в кристаллическом, редуцированном, неразложимом RootPairing при IsValuedIn знак отношения lt обеспечивает pairingIn i j ≤ 0 тогда и только тогда, когда pairingIn j i ≤ 0.

LaTeX

$$$ P.pairingIn S i j \le 0 \iff P.pairingIn S j i \le 0 $$$

Lean4

theorem zero_le_pairingIn_of_root_sub_mem [P.IsNotG2] (h : P.root i - P.root j ∈ range P.root) :
    0 ≤ P.pairingIn ℤ i j :=
  by
  replace h : P.root i + P.root (P.reflectionPerm j j) ∈ range P.root := by simpa [← sub_eq_add_neg]
  simpa using P.pairingIn_le_zero_of_root_add_mem h

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