LeanPool.Monsky.MainStatement

Imported Lean Pool material for LeanPool.Monsky.MainStatement.

theorem LeanPool.Monsky.monsky_theorem (n : ℕ) : (∃ (S : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))), closedHull unitSquare = ⋃ Δ ∈ S, closedHull Δ ∧ (↑S).PairwiseDisjoint openHull ∧ (∀ Δ₁ ∈ S, ∀ Δ₂ ∈ S, MeasureTheory.volume (openHull Δ₁) = MeasureTheory.volume (openHull Δ₂)) ∧ S.card = n) ↔ n ≠ 0 ∧ Even n