def
definition
def or abbrev
brgcPath
show as:
view Lean formalization →
formal statement (Lean)
52def brgcPath : (d : Nat) → Fin (2 ^ d) → Pattern d
53 | 0, _ =>
54 -- unique 0-bit pattern
55 fun _ => False
56 | (d + 1), i =>
57 let T : Nat := 2 ^ d
proof body
Definition body.
58 let hTT : 2 ^ (d + 1) = T + T := by
59 simpa [T, twoPow_succ_eq_add d]
60 let i' : Fin (T + T) := i.cast hTT
61 let left : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d k) false
62 let right : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d (Fin.rev k)) true
63 Fin.append left right i'
64
65/-! ## Injectivity (no repeats) -/
66