pith. machine review for the scientific record. sign in
def definition def or abbrev

brgcGrayCover

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)

 431noncomputable def brgcGrayCover (d : Nat) (hdpos : 0 < d) : GrayCover d (2 ^ d) :=

proof body

Definition body.

 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

used by (3)

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

depends on (14)

Lean names referenced from this declaration's body.