`BookProof.ChapterAttentionCollision.effectiveSupport_le_card` {p : Fin m → ℝ} (hsum : ∑ j, p j = 1) : effectiveSupport p ≤ (m : ℝ)

Initializing...

`BookProof.ChapterAttentionCollision.effectiveSupport_le_card` {p : Fin m → ℝ} (hsum : ∑ j, p j = 1) : effectiveSupport p ≤ (m : ℝ) · Prove2Me