def DecomposingCoverings.IsCovering {ι : Type u_1} (center : ι → E3) : Prop

A family of unit balls with centres center is a covering of $\mathbb{R}^3$ when every point is covered by at least one ball.

def DecomposingCoverings.IsDecomposable {ι : Type u_1} (center : ι → E3) : Prop

A family of unit balls is decomposable if its index set can be partitioned into two classes $A$ and $A^c$ such that both subfamilies still cover $\mathbb{R}^3$.

theorem DecomposingCoverings.theorem_6_2_12 {ι : Type u_1} (center : ι → E3) (k : ℕ) (hk : 2 ≤ k) (hcov : IsKFoldCovering center k) (hindec : ¬IsDecomposable center) : ∃ (x : E3), 2 ^ (↑k / 3) ≤ ↑(mult center x)

Theorem 6.2.12 (Mani-Levitska, Pach 1986). Any $k$-fold covering of $\mathbb{R}^3$ by unit balls that cannot be split into two coverings must cover some point at least $2^{k/3}$ times.