Bridge to Mathlib's Huang Theorem

Repackages Mathlib's Sensitivity.huang_degree_theorem in terms compatible with our definitions.

The Mathlib formalization in Archive.Sensitivity originates from the lean-sensitivity project, a rapid community formalization of Huang's proof carried out shortly after the paper appeared in 2019. That effort was a key inspiration for this project.

theorem Sensitivity.huang_finset {m : ℕ} (H : Finset (Fin (m + 1) → Bool)) (hH : 2 ^ m + 1 ≤ H.card) : ∃ q ∈ H, √(↑m + 1) ≤ ↑{p ∈ H | ∃ (i : Fin (m + 1)), p = flipBit q i}.card

Mathlib's Huang theorem restated with Finsets.