GeometricUtils

📁 Source: BanachTarski/GeometricUtils.lean

Statistics

Metric	Count
Definitions `B3`, `B3min`, `Bad`, `BadAt`, `BadAtN`, `BadAtN_rot`, `BadAtN_rot_iso`, `BadEl`, `G3`, `IccT`, `MAT1`, `S2_sub`, `SO3_embed_G3`, `SO3_in_G3`, `SO3_into_G3`, `SO3_to_G3_iso_forward_equiv`, `ToEquivSO3`, `cone`, `hmo`, `instMulActionG3R3`, `is_s2`, `orbit`, `origin_in_s`, `skew_rot`, `to_s2`, `to_s2_r3`, `trunc_cone`, `v2m`, `x_axis`, `x_axis_vec`	30
Theorems `BadAtN_rot_iso_countable`, `BadAtN_rot_iso_equiv`, `BadAtN_skew_rot`, `BadAtN_skew_rot_countable`, `SO3_G3_action_equiv`, `b3min_is_trunc_cone_s2`, `bad_as_union`, `bad_as_union_rot`, `bad_as_union_skew_rot`, `collapse_iter`, `cone_lemma`, `conj_bad_el`, `countable_bad_rots`, `countable_bad_skew_rot`, `cover_lemma`, `disj_lemma`, `dot_as_matmul`, `dp_nonneg`, `f_triv_g3`, `hmo_is_bijective`, `hmo_is_injective`, `hmo_is_surjective`, `ih`, `instSMulCommClassRealSubtypeMatrixFinOfNatNatMemSubmonoidSO3R3`, `interval_uncountable`, `isometry_of_so3`, `lb_card_s2`, `map_lemma`, `origin_cont`, `rot_containment_S2`, `rot_containment_general`, `rot_iso_comp_add`, `rot_iso_fixed`, `rot_iso_fixed_gen`, `rot_iso_power_lemma`, `s2_uncountable`, `same_bad`, `skew_rot_comp_add`, `skew_rot_power_lemma`, `so3_cancel_lem`, `so3_diff_lin`, `so3_fixes_norm`, `so3_fixes_s2`, `srot_containment`, `triv_so3`, `trunc_cone_lemma`, `trunc_cone_sub_ball`, `v2m_equiv`, `x_axis_on_sphere`	49
Total	79

(root)

Definitions

Name	Category	Theorems
`B3` 📖	CompOp	2 math math: `srot_containment`, `banach_tarski_paradox_B3`
`B3min` 📖	CompOp	3 math math: `b3min_is_trunc_cone_s2`, `banach_tarski_paradox_B3_minus_origin`, `trunc_cone_sub_ball`
`Bad` 📖	CompOp	5 math math: `countable_bad_skew_rot`, `countable_bad_rots`, `bad_as_union_rot`, `bad_as_union_skew_rot`, `bad_as_union`
`BadAt` 📖	CompOp	1 math math: `bad_as_union`
`BadAtN` 📖	CompOp	4 math math: `BadAtN_skew_rot_countable`, `bad_as_union_rot`, `BadAtN_skew_rot`, `bad_as_union_skew_rot`
`BadAtN_rot` 📖	CompOp	1 math math: `same_bad`
`BadAtN_rot_iso` 📖	CompOp	3 math math: `BadAtN_rot_iso_equiv`, `same_bad`, `BadAtN_rot_iso_countable`
`BadEl` 📖	MathDef	1 math math: `conj_bad_el`
`G3` 📖	CompOp	14 math math: `countable_bad_skew_rot`, `hmo_is_surjective`, `BadAtN_skew_rot_countable`, `srot_containment`, `banach_tarski_paradox_B3`, `skew_rot_comp_add`, `BadAtN_skew_rot`, `origin_cont`, `f_triv_g3`, `SO3_G3_action_equiv`, `bad_as_union_skew_rot`, `hmo_is_bijective`, `hmo_is_injective`, `skew_rot_power_lemma`
`IccT` 📖	CompOp	2 math math: `ih`, `interval_uncountable`
`MAT1` 📖	CompOp	2 math math: `v2m_equiv`, `dot_as_matmul`
`S2_sub` 📖	CompOp	—
`SO3_embed_G3` 📖	CompOp	—
`SO3_in_G3` 📖	CompOp	3 math math: `hmo_is_surjective`, `hmo_is_bijective`, `hmo_is_injective`
`SO3_into_G3` 📖	CompOp	1 math math: `SO3_G3_action_equiv`
`SO3_to_G3_iso_forward_equiv` 📖	CompOp	—
`ToEquivSO3` 📖	CompOp	—
`cone` 📖	CompOp	1 math math: `cone_lemma`
`hmo` 📖	CompOp	3 math math: `hmo_is_surjective`, `hmo_is_bijective`, `hmo_is_injective`
`instMulActionG3R3` 📖	CompOp	8 math math: `countable_bad_skew_rot`, `BadAtN_skew_rot_countable`, `srot_containment`, `banach_tarski_paradox_B3`, `BadAtN_skew_rot`, `f_triv_g3`, `SO3_G3_action_equiv`, `bad_as_union_skew_rot`
`is_s2` 📖	CompOp	—
`orbit` 📖	CompOp	2 math math: `srot_containment`, `rot_containment_general`
`origin_in_s` 📖	CompOp	3 math math: `BadAtN_skew_rot_countable`, `BadAtN_skew_rot`, `bad_as_union_skew_rot`
`skew_rot` 📖	CompOp	9 math math: `countable_bad_skew_rot`, `BadAtN_skew_rot_countable`, `srot_containment`, `skew_rot_comp_add`, `BadAtN_skew_rot`, `origin_cont`, `f_triv_g3`, `bad_as_union_skew_rot`, `skew_rot_power_lemma`
`to_s2` 📖	CompOp	1 math math: `ih`
`to_s2_r3` 📖	CompOp	—
`trunc_cone` 📖	CompOp	5 math math: `cover_lemma`, `map_lemma`, `disj_lemma`, `b3min_is_trunc_cone_s2`, `trunc_cone_sub_ball`
`v2m` 📖	CompOp	2 math math: `v2m_equiv`, `dot_as_matmul`
`x_axis` 📖	CompOp	—
`x_axis_vec` 📖	CompOp	1 math math: `x_axis_on_sphere`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`BadAtN_rot_iso_countable` 📖	mathematical	`R3` `S2`	`BadAtN_rot_iso`	—	`BadAtN_rot_iso_equiv`
`BadAtN_rot_iso_equiv` 📖	mathematical	`R3` `S2`	`BadAtN_rot_iso` `ang_diff`	—	`rot_iso_power_lemma` `rot_iso_fixed_gen`
`BadAtN_skew_rot` 📖	mathematical	—	`BadAtN` `R3` `G3` `instMulActionG3R3` `skew_rot` `origin` `origin_in_s`	—	`f_triv_g3` `skew_rot_power_lemma` `operp.eq_1` `origin.eq_1` `rot_iso_fixed` `rot_iso_fixed_back`
`BadAtN_skew_rot_countable` 📖	mathematical	—	`BadAtN` `R3` `G3` `instMulActionG3R3` `skew_rot` `origin` `origin_in_s`	—	`BadAtN_skew_rot`
`SO3_G3_action_equiv` 📖	mathematical	—	`G3` `R3` `instMulActionG3R3` `SO3_into_G3` `SO3`	—	—
`b3min_is_trunc_cone_s2` 📖	mathematical	—	`B3min` `trunc_cone` `R3` `S2`	—	—
`bad_as_union` 📖	mathematical	—	`Bad` `BadAt`	—	—
`bad_as_union_rot` 📖	mathematical	`R3` `S2`	`Bad` `SO3` `SO3_action_on_R3` `rot` `BadAtN`	—	`bad_as_union`
`bad_as_union_skew_rot` 📖	mathematical	—	`Bad` `R3` `G3` `instMulActionG3R3` `skew_rot` `origin` `BadAtN` `origin_in_s`	—	`bad_as_union`
`collapse_iter` 📖	mathematical	—	`f`	—	—
`cone_lemma` 📖	mathematical	—	`R3` `cone` `S2` `normed`	—	—
`conj_bad_el` 📖	mathematical	—	`BadEl` `f`	—	`collapse_iter`
`countable_bad_rots` 📖	mathematical	`R3` `S2`	`Bad` `SO3` `SO3_action_on_R3` `rot`	—	`bad_as_union_rot` `same_bad` `BadAtN_rot_iso_countable`
`countable_bad_skew_rot` 📖	mathematical	—	`Bad` `R3` `G3` `instMulActionG3R3` `skew_rot` `origin`	—	`bad_as_union_skew_rot` `BadAtN_skew_rot_countable`
`cover_lemma` 📖	mathematical	`R3` `S2`	`trunc_cone`	—	`trunc_cone_lemma` `cone_lemma`
`disj_lemma` 📖	mathematical	`R3` `S2`	`trunc_cone`	—	`trunc_cone_lemma`
`dot_as_matmul` 📖	mathematical	—	`MAT1` `v2m`	—	—
`dp_nonneg` 📖	—	—	—	—	—
`f_triv_g3` 📖	mathematical	—	`f` `R3` `G3` `instMulActionG3R3` `skew_rot`	—	—
`hmo_is_bijective` 📖	mathematical	—	`SO3` `G3` `R3` `SO3_in_G3` `hmo`	—	`hmo_is_injective` `hmo_is_surjective`
`hmo_is_injective` 📖	mathematical	—	`SO3` `G3` `R3` `SO3_in_G3` `hmo`	—	`isometry_of_so3`
`hmo_is_surjective` 📖	mathematical	—	`SO3` `G3` `R3` `SO3_in_G3` `hmo`	—	—
`ih` 📖	mathematical	—	`IccT` `R3` `S2` `to_s2`	—	—
`instSMulCommClassRealSubtypeMatrixFinOfNatNatMemSubmonoidSO3R3` 📖	mathematical	—	`SO3` `R3`	—	—
`interval_uncountable` 📖	mathematical	—	`IccT`	—	—
`isometry_of_so3` 📖	mathematical	—	`R3` `f` `SO3` `SO3_action_on_R3`	—	`so3_diff_lin` `so3_fixes_norm`
`lb_card_s2` 📖	mathematical	—	`R3` `S2`	—	`s2_uncountable`
`map_lemma` 📖	mathematical	`R3` `f` `SO3` `SO3_action_on_R3` `S2`	`trunc_cone`	—	`instSMulCommClassRealSubtypeMatrixFinOfNatNatMemSubmonoidSO3R3` `so3_fixes_norm`
`origin_cont` 📖	mathematical	—	`R3` `G3` `skew_rot` `origin`	—	—
`rot_containment_S2` 📖	mathematical	—	`R3` `f` `SO3` `SO3_action_on_R3` `rot` `S2`	—	`so3_fixes_s2`
`rot_containment_general` 📖	mathematical	`R3` `S2`	`orbit` `SO3` `SO3_action_on_R3` `rot`	—	`rot_containment_S2`
`rot_iso_comp_add` 📖	mathematical	—	`R3` `rot_iso`	—	`rot_by_parts_comp`
`rot_iso_fixed` 📖	—	`R3` `rot_iso`	—	—	`rot_iso_fixed_gen` `orth_dim_2`
`rot_iso_fixed_gen` 📖	mathematical	`R3` `rot_iso`	`ang_diff`	—	`orth_dim_2` `operp_spar` `operp_up` `operp_add`
`rot_iso_power_lemma` 📖	mathematical	—	`R3` `rot_iso`	—	`triv_rot_iso` `rot_iso_comp_add`
`s2_uncountable` 📖	mathematical	—	`R3` `S2`	—	`interval_uncountable` `ih`
`same_bad` 📖	mathematical	—	`BadAtN_rot` `BadAtN_rot_iso`	—	`rot_pow_lemma` `rot_iso_pow_lemma` `same_action`
`skew_rot_comp_add` 📖	mathematical	—	`R3` `G3` `skew_rot`	—	`rot_iso_comp_add`
`skew_rot_power_lemma` 📖	mathematical	—	`R3` `G3` `skew_rot`	—	`triv_rot_iso` `skew_rot_comp_add`
`so3_cancel_lem` 📖	mathematical	—	`SO3`	—	—
`so3_diff_lin` 📖	mathematical	—	`R3` `SO3`	—	—
`so3_fixes_norm` 📖	mathematical	—	`R3` `SO3`	—	`dot_as_matmul` `v2m_equiv` `so3_cancel_lem` `dp_nonneg`
`so3_fixes_s2` 📖	mathematical	—	`R3` `f` `SO3` `SO3_action_on_R3` `S2`	—	`so3_fixes_norm`
`srot_containment` 📖	mathematical	—	`R3` `orbit` `G3` `instMulActionG3R3` `skew_rot` `origin` `B3`	—	`skew_rot_power_lemma` `f_triv_g3` `origin_cont`
`triv_so3` 📖	mathematical	—	`f` `R3` `SO3` `SO3_action_on_R3`	—	—
`trunc_cone_lemma` 📖	mathematical	`R3` `trunc_cone`	`S2` `normed`	—	`cone_lemma`
`trunc_cone_sub_ball` 📖	mathematical	—	`R3` `trunc_cone` `B3min`	—	—
`v2m_equiv` 📖	mathematical	—	`v2m` `MAT` `MAT1`	—	—
`x_axis_on_sphere` 📖	mathematical	—	`R3` `S2` `x_axis_vec`	—	—

---

← Back to Index