Bridge to Mathlib's Finset.Shatters

Equates BinaryMatrix.shatters with Mathlib's Finset.Shatters via the associated toFinsetFamily construction, plus an auxiliary uniqueness lemma for Bool-valued functions on Fin n matched by their true-filter.

theorem BinaryMatrix.shatters_iff {m n : ℕ} (M : BinaryMatrix m n) (S : Finset (Fin n)) : M.shatters S ↔ M.toFinsetFamily.Shatters S

shatters coincides with Mathlib's Finset.Shatters on the associated Finset family.

theorem BinaryMatrix.bool_fun_eq_of_filter_eq {n : ℕ} (f g : Fin n → Bool) (h : {j : Fin n | f j = true} = {j : Fin n | g j = true}) : f = g

Two Bool-valued functions on Fin n are equal if they have the same univ.filter-set of true indices.