Finset Helper Lemmas

General-purpose lemmas about Finsets and Fin types.

Main Results

• Finset.filter_val_lt_card: Cardinality of filtered Fin elements by value bound

theorem Finset.filter_val_lt_card {m n : ℕ} (h : m ≥ n) : {i : Fin m | ↑i < n}.card = n

Cardinality of filtered Fin elements.

For m ≥ n, the number of elements i : Fin m with i.val < n is exactly n.

This is because Fin m = {0, 1, ..., m-1} contains all of {0, 1, ..., n-1} when m ≥ n, and these are precisely the elements satisfying i.val < n.

The proof uses an explicit bijection between Fin n and the filtered set.