lemma proved term proof

`restrict_enc_true`

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

formal statement (Lean)

  27@[simp] lemma restrict_enc_true (R : Fin n → Bool) (M : Finset (Fin n)) :
  28  restrict (n:=n) (enc true R) M = (fun i => ! (restrict (n:=n) R M i)) := by

proof body

Term-mode proof.

  29  funext i; simp [restrict, enc]
  30
  31/-- Extend a partial assignment on `M` to a full mask by defaulting to `false` off `M`. -/

depends on (4)

Lean names referenced from this declaration's body.

enc in IndisputableMonolith.Complexity.BalancedParityHidden decl_use
restrict in IndisputableMonolith.Complexity.BalancedParityHidden decl_use
M in IndisputableMonolith.Recognition decl_use
M in IndisputableMonolith.Recognition.Cycle3 decl_use