Words agreeing off a set of positions

The words ι → Bool agreeing with a word x outside a set F of positions are free exactly on F, so there are 2 ^ |F| of them (BitString.card_filter_forall_notMem_eq).

Main results

• Cslib.BitString.card_filter_forall_notMem_eq: the words agreeing with x outside F number 2 ^ |F|.

theorem Cslib.BitString.card_filter_forall_notMem_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : Finset ι) (x : ι → Bool) [DecidablePred fun (y : ι → Bool) => ∀ i ∉ F, y i = x i] : {y : ι → Bool | ∀ i ∉ F, y i = x i}.card = 2 ^ F.card

The words agreeing with x outside F number 2 ^ |F|.