session "Banach_Tarski" (AFP) = "HOL-Analysis" +
description ‹
The Banach-Tarski paradox: the closed unit ball in three-dimensional
Euclidean space admits a finite paradoxical decomposition under
isometries. This is the main submission session; it is checked with
complete proof terms and the AFP mandatory lint bundle. ›
options [timeout = 600]
sessions "Free-Groups"
theories
BT_Prelim
Paradoxical_Decomposition
Free_Action_Paradox
Free_Group_F2
F2_Paradox
Free_Rotations_SO3
Hausdorff_Paradox
Sphere_Decomposition
Ball_Decomposition
Banach_Tarski_Theorem
document_files "root.tex" "root.bib"
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet am 2026-09-10)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
