lemma proved wrapper

`extendMask_in`

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

formal statement (Lean)

  35@[simp] lemma extendMask_in (M : Finset (Fin n)) (a : {i // i ∈ M} → Bool) {i : Fin n} (h : i ∈ M) :
  36  extendMask (n:=n) M a i = a ⟨i, h⟩ := by

proof body

One-line wrapper that applies simp.

  37  simp [extendMask, h]
  38

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