Bridge to Mathlib's Huang Theorem

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

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.