Banach–Tarski paradox

8 fully proved

Equidecomposability

DefinitionFinite equidecomposability by isometries#✓fully proved

Let \(X\) be a metric space. Subsets \(A\) and \(B\) of \(X\) are finitely equidecomposable by isometries if there are a natural number \(n\), sets \(A_1, \dots, A_n\) and \(B_1, \dots, B_n\) in \(X\), and isometric bijections \(g_1, \dots, g_n\) of \(X\) onto itself such that the sets \(A_i\) are pairwise disjoint, the sets \(B_i\) are pairwise disjoint, \(A = A_1 \cup \dots \cup A_n\), \(B = B_1 \cup \dots \cup B_n\), and \(g_i(A_i) = B_i\) for every \(i\).

def FinitelyEquidecomposableByIsometries
    {X : Type*} [MetricSpace X] (A B : Set X) : Prop :=
  ∃ (n : ℕ) (As : Fin n → Set X) (Bs : Fin n → Set X) (gs : Fin n → X ≃ᵢ X),
    (∀ i j, i ≠ j → Disjoint (As i) (As j)) ∧
    (∀ i j, i ≠ j → Disjoint (Bs i) (Bs j)) ∧
    (⋃ i, As i) = A ∧
    (⋃ i, Bs i) = B ∧
    ∀ i, (gs i : X → X) '' As i = Bs i

Used by 7

Used byBanach–Tarski paradox for the closed unit ball · Equidecomposability via piecewise-isometric bijections · Equidecomposability of a set with its isometric image · Finite equidecomposability by isometries is reflexive · Finite equidecomposability by isometries is symmetric · Finite equidecomposability by isometries is transitive · Finite equidecomposability by isometries respects disjoint unions

TheoremEquidecomposability via piecewise-isometric bijections#✓fully proved

Let \(A\) and \(B\) be subsets of a metric space \(X\). Then \(A\) is finitely equidecomposable by isometries with \(B\) if and only if there are a map \(f : X \to X\) and a finite set \(S\) of isometric bijections of \(X\) onto itself such that \(f\) restricts to a bijection from \(A\) onto \(B\) and for every \(x \in A\) there is \(g \in S\) with \(f(x) = g(x)\).

public theorem finitelyEquidecomposableByIsometries_iff_bijOn
    {X : Type*} [MetricSpace X] (A B : Set X) :
    FinitelyEquidecomposableByIsometries A B ↔
      ∃ (f : X → X) (S : Set (X ≃ᵢ X)),
        S.Finite ∧ Set.BijOn f A B ∧ ∀ x ∈ A, ∃ g ∈ S, f x = g x

Uses 1

Statement usesFinite equidecomposability by isometries

Finitely Equidecomposable By Isometries

TheoremFinite equidecomposability by isometries is reflexive#✓fully proved

Every subset \(A\) of a metric space \(X\) is finitely equidecomposable by isometries with itself.

public theorem refl {X : Type*} [MetricSpace X] (A : Set X) :
    FinitelyEquidecomposableByIsometries A A

Uses 1

Statement usesFinite equidecomposability by isometries

TheoremFinite equidecomposability by isometries is symmetric#✓fully proved

Let \(A\) and \(B\) be subsets of a metric space \(X\). If \(A\) is finitely equidecomposable by isometries with \(B\), then \(B\) is finitely equidecomposable by isometries with \(A\).

public theorem symm {X : Type*} [MetricSpace X] {A B : Set X}
    (h : FinitelyEquidecomposableByIsometries A B) :
    FinitelyEquidecomposableByIsometries B A

Uses 1

Statement usesFinite equidecomposability by isometries

TheoremFinite equidecomposability by isometries is transitive#✓fully proved

Let \(A\), \(B\) and \(C\) be subsets of a metric space \(X\). If \(A\) is finitely equidecomposable by isometries with \(B\) and \(B\) is finitely equidecomposable by isometries with \(C\), then \(A\) is finitely equidecomposable by isometries with \(C\).

public theorem trans {X : Type*} [MetricSpace X] {A B C : Set X}
    (h1 : FinitelyEquidecomposableByIsometries A B)
    (h2 : FinitelyEquidecomposableByIsometries B C) :
    FinitelyEquidecomposableByIsometries A C

Uses 1

Statement usesFinite equidecomposability by isometries

TheoremFinite equidecomposability by isometries respects disjoint unions#✓fully proved

Let \(A_1\), \(A_2\), \(B_1\) and \(B_2\) be subsets of a metric space \(X\) with \(A_1 \cap A_2 = \emptyset\) and \(B_1 \cap B_2 = \emptyset\). If \(A_1\) is finitely equidecomposable by isometries with \(B_1\) and \(A_2\) is finitely equidecomposable by isometries with \(B_2\), then \(A_1 \cup A_2\) is finitely equidecomposable by isometries with \(B_1 \cup B_2\).

public theorem union {X : Type*} [MetricSpace X] {A₁ A₂ B₁ B₂ : Set X}
    (h1 : FinitelyEquidecomposableByIsometries A₁ B₁)
    (h2 : FinitelyEquidecomposableByIsometries A₂ B₂)
    (hdA : Disjoint A₁ A₂) (hdB : Disjoint B₁ B₂) :
    FinitelyEquidecomposableByIsometries (A₁ ∪ A₂) (B₁ ∪ B₂)

Uses 1

Statement usesFinite equidecomposability by isometries

TheoremEquidecomposability of a set with its isometric image#✓fully proved

Let \(g\) be an isometric bijection of a metric space \(X\) onto itself. Then every subset \(A\) of \(X\) is finitely equidecomposable by isometries with its image \(g(A)\).

public theorem image_isometryEquiv {X : Type*} [MetricSpace X]
    (g : X ≃ᵢ X) (A : Set X) :
    FinitelyEquidecomposableByIsometries A (g '' A)

Uses 1

Statement usesFinite equidecomposability by isometries

Banach–Tarski paradox

TheoremBanach–Tarski paradox for the closed unit ball#✓fully proved

In three-dimensional Euclidean space \(\mathbb{R}^3\), write \(\bar B(c, r)\) for the closed ball of radius \(r\) about \(c\). There are points \(c_1, c_2 \in \mathbb{R}^3\) such that \(\bar B(c_1, 1)\) and \(\bar B(c_2, 1)\) are disjoint and the closed unit ball \(\bar B(0, 1)\) is finitely equidecomposable by isometries with \(\bar B(c_1, 1) \cup \bar B(c_2, 1)\).

public theorem banach_tarski_closedBall_unit :
    ∃ (c₁ c₂ : EuclideanSpace ℝ (Fin 3)),
      Disjoint (Metric.closedBall c₁ 1) (Metric.closedBall c₂ 1) ∧
      FinitelyEquidecomposableByIsometries
        (Metric.closedBall (0 : EuclideanSpace ℝ (Fin 3)) 1)
        (Metric.closedBall c₁ 1 ∪ Metric.closedBall c₂ 1)

Sources

• S. Banach and A. Tarski, Fund. Math. 6 (1924) 244–277 original paradox; S. Wagon, The Banach–Tarski Paradox, Cambridge Univ. Press (1993); Lean states closed unit ball duplication specialization in ℝ³ with ambient ≃ᵢ equidecomposability.

Uses 1

Statement usesFinite equidecomposability by isometries

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.