7.1 Binary matrix setup

Definition 7.1 Binary matrix

Lean: BinaryMatrix

\(\mathrm{BinaryMatrix}\, m\, n \; :=\; \mathrm{Fin}\, m \to \mathrm{Fin}\, n \to \mathrm{Bool}\). Type-definitionally equal to \(\mathrm{Matrix}\, (\mathrm{Fin}\, m)\, (\mathrm{Fin}\, n)\, \mathrm{Bool}\).

Definition 7.2 Induced set family

Lean: BinaryMatrix.toFinsetFamily

The induced set family of a binary matrix \(M : \mathrm{Fin}\, m \to \mathrm{Fin}\, n \to \mathrm{Bool}\) consists of the true-supports of its rows, \(\{ \{ j : M\, i\, j = \mathrm{true} \} : i \in \mathrm{Fin}\, m \} \) [ 23 ] , [ 17 ] .

Definition 7.3 Matrix shattering

Lean: BinaryMatrix.shatters

For a binary matrix \(M\) and \(S \subseteq \mathrm{Fin}\, n\), \(M\) shatters \(S\) iff every pattern \(t \subseteq S\) is realized by some row of \(M\) [ 23 ] , [ 17 ] .

Theorem 7.4 Consistency with Finset.Shatters

Lean: BinaryMatrix.shatters_iff

\(M\) shatters \(S \iff \mathrm{toFinsetFamily}\, M\) shatters \(S\) in Mathlib’s sense [ 17 ] .

Lemma 7.5 Boolean function equality via filter

Lean: BinaryMatrix.bool_fun_eq_of_filter_eq

Two Boolean-valued functions \(f, g : \mathrm{Fin}\, n \to \mathrm{Bool}\) with equal true-filters are equal.