theorem
proved
wrapper
grayCover_min_ticks
show as:
view Lean formalization →
formal statement (Lean)
68theorem grayCover_min_ticks {d T : Nat} [NeZero T] (w : GrayCover d T) : 2 ^ d ≤ T :=
proof body
One-line wrapper that applies Patterns.min_ticks_cover.
69 Patterns.min_ticks_cover (d := d) (T := T) w.path w.complete
70