lemma proved term proof

`restrict_enc_false`

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

formal statement (Lean)

  23@[simp] lemma restrict_enc_false (R : Fin n → Bool) (M : Finset (Fin n)) :
  24  restrict (n:=n) (enc false R) M = restrict (n:=n) R M := by

Term-mode proof.

  25  funext i; simp [restrict, enc]
  26

Lean names referenced from this declaration's body.