not_isG2_iff_isNotG2 — Mathlib

English

The same equivalence holds: not IsG2 is equivalent to IsNotG2, under crystallographic assumptions.

Русский

Те же эквивалентности: не IsG2 эквивалентно IsNotG2 при кристаллизационных предпосылках.

LaTeX

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

Lean4

@[simp]
theorem not_isG2_iff_isNotG2 : ¬P.IsG2 ↔ P.IsNotG2 :=
  by
  simp only [isG2_iff, isNotG2_iff, not_exists, Set.mem_insert_iff, mem_singleton_iff]
  refine ⟨fun h i j ↦ ?_, fun h i j ↦ ?_⟩
  · have hij := h (P.reflectionPerm i i) j
    have := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed i j
    aesop
  · specialize h i j
    cutsat

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