Documentation Verification Report

Basic

📁 Source: BanachTarski/Basic.lean

Statistics

Metric	Count
Definitions `Equidecomposible`, `FixedPoints`, `Paradoxical`, `SelfParadoxical`	4
Theorems `S2_equidecomposible_of_S2_minus_countable`, `absorption_lemma_1`, `absorption_lemma_2`, `absorption_lemma_3`, `banach_tarski_paradox_B3`, `banach_tarski_paradox_B3_minus_origin`, `banach_tarski_paradox_s2`, `equidecomposibility_symm`, `equidecomposibility_trans`, `equidecomposible_of_supergroup_of_equidecomposible`, `free_group_of_rank_two_is_self_paradoxical`, `hausdorff_paradox`, `paradoxical_of_action_of_self_paradoxical`, `paradoxical_of_equidecomposible_of_paradoxical`, `paradoxical_of_supergroup_of_paradoxical`, `paradoxical_preserved_by_iso`, `self_paradoxical_preserved_by_iso`	17
Total	21

(root)

Definitions

Name	Category	Theorems
`Equidecomposible` 📖	MathDef	4 math math: `S2_equidecomposible_of_S2_minus_countable`, `absorption_lemma_3`, `absorption_lemma_1`, `absorption_lemma_2`
`FixedPoints` 📖	CompOp	—
`Paradoxical` 📖	MathDef	5 math math: `paradoxical_of_action_of_self_paradoxical`, `hausdorff_paradox`, `banach_tarski_paradox_B3`, `banach_tarski_paradox_s2`, `banach_tarski_paradox_B3_minus_origin`
`SelfParadoxical` 📖	MathDef	1 math math: `free_group_of_rank_two_is_self_paradoxical`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`S2_equidecomposible_of_S2_minus_countable` 📖	mathematical	`R3` `S2`	`Equidecomposible` `SO3` `SO3_action_on_R3`	—	`lb_card_s2` `countable_bad_rots` `equidecomposibility_symm` `absorption_lemma_3` `rot_containment_general`
`absorption_lemma_1` 📖	mathematical	`f`	`Equidecomposible`	—	`split2`
`absorption_lemma_2` 📖	mathematical	`f`	`Equidecomposible`	—	`absorption_lemma_1`
`absorption_lemma_3` 📖	mathematical	`Bad` `orbit`	`Equidecomposible`	—	`absorption_lemma_2`
`banach_tarski_paradox_B3` 📖	mathematical	—	`Paradoxical` `R3` `G3` `instMulActionG3R3` `B3`	—	`paradoxical_preserved_by_iso` `SO3_G3_action_equiv` `banach_tarski_paradox_B3_minus_origin` `paradoxical_of_supergroup_of_paradoxical` `countable_bad_skew_rot` `srot_containment` `absorption_lemma_3` `paradoxical_of_equidecomposible_of_paradoxical` `equidecomposibility_symm`
`banach_tarski_paradox_B3_minus_origin` 📖	mathematical	—	`Paradoxical` `R3` `SO3` `SO3_action_on_R3` `B3min`	—	`banach_tarski_paradox_s2` `disj_lemma` `cover_lemma` `b3min_is_trunc_cone_s2` `map_lemma` `trunc_cone_sub_ball` `trunc_cone_lemma`
`banach_tarski_paradox_s2` 📖	mathematical	—	`Paradoxical` `R3` `SO3` `SO3_action_on_R3` `S2`	—	`hausdorff_paradox` `S2_equidecomposible_of_S2_minus_countable` `paradoxical_of_equidecomposible_of_paradoxical`
`equidecomposibility_symm` 📖	—	`Equidecomposible`	—	—	—
`equidecomposibility_trans` 📖	—	`Equidecomposible`	—	—	`ml` `ml2` `fcomp`
`equidecomposible_of_supergroup_of_equidecomposible` 📖	—	`Equidecomposible`	—	—	—
`free_group_of_rank_two_is_self_paradoxical` 📖	mathematical	—	`SelfParadoxical` `FG2`	—	`split2` `wopts`
`hausdorff_paradox` 📖	mathematical	—	`R3` `S2` `Paradoxical` `SO3` `SO3_action_on_R3`	—	`self_paradoxical_preserved_by_iso` `free_group_of_rank_two_is_self_paradoxical` `countable_of_fg2` `fixed_lemma` `so3_fixes_s2` `lb_card_s2` `FixedPoints.eq_1` `paradoxical_of_action_of_self_paradoxical` `paradoxical_of_supergroup_of_paradoxical`
`paradoxical_of_action_of_self_paradoxical` 📖	mathematical	`f` `SelfParadoxical` `FixedPoints`	`Paradoxical`	—	—
`paradoxical_of_equidecomposible_of_paradoxical` 📖	—	`Paradoxical` `Equidecomposible`	—	—	`equidecomposibility_trans` `equidecomposibility_symm`
`paradoxical_of_supergroup_of_paradoxical` 📖	—	`Paradoxical`	—	—	`equidecomposible_of_supergroup_of_equidecomposible`
`paradoxical_preserved_by_iso` 📖	—	`Paradoxical`	—	—	—
`self_paradoxical_preserved_by_iso` 📖	—	`SelfParadoxical`	—	—	`paradoxical_preserved_by_iso`

---

← Back to Index