pith. machine review for the scientific record. sign in
theorem proved tactic proof

grayCycle3_bijective

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 137theorem grayCycle3_bijective : Function.Bijective grayCycle3Path := by

proof body

Tactic-mode proof.

 138  classical
 139  -- card(Fin 8) = 8
 140  have hFin : Fintype.card (Fin 8) = 8 := by simp
 141  -- card(Pattern 3) = 2^3 = 8
 142  have hPat' : Fintype.card (Pattern 3) = 2 ^ 3 := by
 143    simpa using (Patterns.card_pattern 3)
 144  have hPow : (2 ^ 3 : Nat) = 8 := by decide
 145  have hPat : Fintype.card (Pattern 3) = 8 := by simpa [hPow] using hPat'
 146  have hcard : Fintype.card (Fin 8) = Fintype.card (Pattern 3) := by
 147    -- rewrite both sides to 8
 148    calc
 149      Fintype.card (Fin 8) = 8 := hFin
 150      _ = Fintype.card (Pattern 3) := by simpa [hPat]
 151  -- injective + card equality ⇒ bijective
 152  exact (Fintype.bijective_iff_injective_and_card grayCycle3Path).2 ⟨grayCycle3_injective, hcard⟩
 153

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.