lemma proved wrapper

`extendMask_notin`

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

formal statement (Lean)

  39@[simp] lemma extendMask_notin (M : Finset (Fin n)) (a : {i // i ∈ M} → Bool) {i : Fin n} (h : i ∉ M) :
  40  extendMask (n:=n) M a i = false := by

proof body

One-line wrapper that applies simp.

  41  simp [extendMask, h]
  42

depends on (3)

Lean names referenced from this declaration's body.

extendMask in IndisputableMonolith.Complexity.BalancedParityHidden decl_use
M in IndisputableMonolith.Recognition decl_use
M in IndisputableMonolith.Recognition.Cycle3 decl_use