def definition def or abbrev

`extendMask`

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

formal statement (Lean)

  32def extendMask (M : Finset (Fin n)) (a : {i // i ∈ M} → Bool) : Fin n → Bool :=

Definition body.

  33  fun i => if h : i ∈ M then a ⟨i, h⟩ else false
  34

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

extendMask_in in IndisputableMonolith.Complexity.BalancedParityHidden decl_use
extendMask_notin in IndisputableMonolith.Complexity.BalancedParityHidden decl_use
restrict_extendMask in IndisputableMonolith.Complexity.BalancedParityHidden decl_use

Lean names referenced from this declaration's body.