isNotG2_iff — Mathlib

English

For crystallographic, reduced, irreducible P, the negation of IsG2 is equivalent to IsNotG2.

Русский

Для кристаллографического, редуцированного, неразложимого P отрицание IsG2 эквивалентно IsNotG2.

LaTeX

$$$ \neg P.IsG2 \iff P.IsNotG2 $$$

Lean4

theorem isNotG2_iff : P.IsNotG2 ↔ ∀ i j, P.pairingIn ℤ i j ∈ ({-2, -1, 0, 1, 2} : Set ℤ) :=
  ⟨fun _ ↦ IsNotG2.pairingIn_mem_zero_one_two, fun h ↦ ⟨h⟩⟩

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