Grace/Cumulus/Geometry/Sphere/Paradox.g17

Open in Workbench Download source

Imports

Absorb · Geometry.Hausdorff.Paradox · Algebra.Group.Paradox.Transfer

Declarations

• sphere.paradoxical theorem derivation

Source

1-- The unit sphere is paradoxical under the rotation group, from2-- Hausdorff's paradox and the absorption of the countable fixed set3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Geometry.Sphere.Paradox9import Absorb10import Geometry.Hausdorff.Paradox11import Algebra.Group.Paradox.Transfer1213theorem sphere.paradoxical14  shows Paradoxical(sphereAction, SO3, S²)15proof16  have action := sphereAction.action17  have subset := difference.subset_left at S², wordFixedSet18  have whole := sphere.absorb_any19    with wordFixedSet.countable, wordFixedSet.subset20  exact Paradoxical.of_equidecomposable21    with action, subset, whole, hausdorff.pieces22