`brgcGrayCycle`

definition

show as: view math explainer →

module: IndisputableMonolith.Patterns.GrayCycleBRGC
domain: Patterns
line: 425 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Patterns.GrayCycleBRGC on GitHub at line 425.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 422
 423/-! ## Packaged GrayCycle/GrayCover -/
 424
 425noncomputable def brgcGrayCycle (d : Nat) (hdpos : 0 < d) : GrayCycle d :=
 426{ path := brgcPath d
 427  inj := brgcPath_injective d
 428  oneBit_step := brgc_oneBit_step (d := d) hdpos
 429}
 430
 431noncomputable def brgcGrayCover (d : Nat) (hdpos : 0 < d) : GrayCover d (2 ^ d) :=
 432{ path := brgcPath d
 433  complete := by
 434    classical
 435    have h_inj : Function.Injective (brgcPath d) := brgcPath_injective d
 436    have h_card : Fintype.card (Fin (2 ^ d)) = Fintype.card (Pattern d) := by
 437      simp [Patterns.card_pattern]
 438    have h_bij : Function.Bijective (brgcPath d) :=
 439      (Fintype.bijective_iff_injective_and_card (brgcPath d)).2 ⟨h_inj, h_card⟩
 440    exact h_bij.2
 441  oneBit_step := brgc_oneBit_step (d := d) hdpos
 442}
 443
 444end GrayCycleBRGC
 445
 446end Patterns
 447end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.