`BookProof.ChapterGaugeComprehensiveFixing.shift_gaugeFixing_classification` : (IsComprehensiveGaugeFixing (Multiplicative ℤ) unitCell ∧ IsCompleteGaugeFixing' (Multiplicative ℤ) u

Proved

BookProof.ChapterGaugeComprehensiveFixing.shift_gaugeFixing_classification

by leonardopedro · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterGaugeComprehensiveFixing.

BookProof.ChapterGaugeComprehensiveFixing.shift_gaugeFixing_classification : (IsComprehensiveGaugeFixing (Multiplicative ℤ) unitCell ∧ IsCompleteGaugeFixing' (Multiplicative ℤ) unitCell) ∧ (IsComprehensiveGaugeFixing (Multiplicative ℤ) (Set.univ : Set ℝ) ∧ ¬ IsCompleteGaugeFixing' (Multiplicative ℤ) (Set.univ : Set ℝ)) ∧ (¬ IsComprehensiveGaugeFixing (Multiplicative ℤ) ({0} : Set ℝ) ∧ IsCompleteGaugeFixing' (Multiplicative ℤ) ({0} : Set ℝ)) ∧ (¬ IsComprehensiveGaugeFixing (Multiplicative ℤ) ({0, 1} : Set ℝ) ∧ ¬ IsCompleteGaugeFixing' (Multiplicative ℤ) ({0, 1} : Set ℝ))

Formalization note: Lean 4 identifier BookProof.ChapterGaugeComprehensiveFixing.shift_gaugeFixing_classification.

Preamble

-- Generated from ChapterGaugeComprehensiveFixing.lean — theorem BookProof.ChapterGaugeComprehensiveFixing.shift_gaugeFixing_classification
import Mathlib
import Definitions.Def_ChapterGaugeComprehensiveFixing
import Definitions.Def_ChapterGaugeIncompleteFixing
open BookProof.ChapterGaugeIncompleteFixing
open BookProof.ChapterGaugeComprehensiveFixing



open BookProof.ChapterGaugeIncompleteFixing

variable {X : Type*} (G : Type*) [Group G] [MulAction G X]
variable {X : Type*} {G : Type*} [Group G] [MulAction G X] {S : Set X}
variable {X : Type*} [TopologicalSpace X] {G : Type*} [Group G] [MulAction G X]
variable (X : Type*) (G : Type*) [Group G] [MulAction G X]

Formal statement

theorem BookProof.ChapterGaugeComprehensiveFixing.shift_gaugeFixing_classification :
    (IsComprehensiveGaugeFixing (Multiplicative ℤ) unitCell ∧
      IsCompleteGaugeFixing' (Multiplicative ℤ) unitCell) ∧
    (IsComprehensiveGaugeFixing (Multiplicative ℤ) (Set.univ : Set ℝ) ∧
      ¬ IsCompleteGaugeFixing' (Multiplicative ℤ) (Set.univ : Set ℝ)) ∧
    (¬ IsComprehensiveGaugeFixing (Multiplicative ℤ) ({0} : Set ℝ) ∧
      IsCompleteGaugeFixing' (Multiplicative ℤ) ({0} : Set ℝ)) ∧
    (¬ IsComprehensiveGaugeFixing (Multiplicative ℤ) ({0, 1} : Set ℝ) ∧
      ¬ IsCompleteGaugeFixing' (Multiplicative ℤ) ({0, 1} : Set ℝ)) := by sorry

View graph