Grace/Cumulus/Geometry/BanachTarski/Strong.g17

Open in Workbench Download source

Imports

Geometry.BanachTarski · Algebra.Group.Paradox.SchroederBernstein

Declarations

Source

1-- The strong form of the Banach–Tarski paradox: the ball is2-- equidecomposable with the disjoint union of two copies of itself3-- 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.BanachTarski.Strong9import Geometry.BanachTarski10import Algebra.Group.Paradox.SchroederBernstein1112-- The ball embeds in the two balls as a subset, the two balls embed in13-- the ball through the part proved in Geometry.BanachTarski, and the14-- Banach–Schröder–Bernstein theorem turns the two embeddings into a15-- decomposition.16theorem banachTarski.two_balls17  shows Equidecomposable(motionAction, Motions, ℝ³, unitBall,18      unitBall ∪ shiftedBall)19proof20  have action := motionAction.action21  obtain ⟨C, boundedC, part⟩ := banachTarski.two_balls_part22  have shiftedSubset : shiftedBall ⊆ ℝ³23    rw shiftedBall.graph24    exact translate.subset at motionAction, ℝ³,25      (matrixRing(realRing, 3)[1], farPoint), unitBall26  have unionSubset := union2.subset with unitBall.subset, shiftedSubset27  have left := union2.subset_left at unitBall, shiftedBall28  have forward :29      Embeds(motionAction, Motions, ℝ³, unitBall, unitBall ∪ shiftedBall) :=30    Embeds.of_subset with action, unitBall.subset, left31  have back := Equidecomposable.symmetric with action, part32  have backward :33      Embeds(motionAction, Motions, ℝ³, unitBall ∪ shiftedBall, unitBall) :=34    Embeds.of_equidecomposable with action, boundedC, back35  exact Equidecomposable.of_embeddings with action, unitBall.subset,36    unionSubset, forward, backward37