The hash family "all functions" has all properties we define. It is completely impractical for pretty much all use-cases (due to being too big).

This file just proves those statements for the sake if illustrating this fact and adding confidence that the definitions are correct.

theorem all_functions_strongly_universal_n {Input : Type u_2} {Output : Type u_3} [Fintype Input] [Fintype Output] [DecidableEq Input] [DecidableEq Output] (n : ℕ) : HashFamily.stronglyUniversal_n n fun (s : Input → Output) (i : Input) => s i

"All functions" as a hash family is strongly-universal-n for any n.