Documentation Verification Report

Common

📁 Source: BanachTarski/Common.lean

Statistics

Metric	Count
Definitions `FG2`, `MAT`, `R3`, `R3_raw`, `S2`, `SO3`, `SO3_action_on_MAT`, `SO3_action_on_R3`, `chartype`, `f`, `normed`, `origin`, `so3_has_inv`, `to_R3`, `σ`, `σchar`, `τ`, `τchar`	18
Theorems `SO3_smul_def`, `countable_chartype`, `countable_of_fg2`, `fcomp`, `finite_chartype`, `finj`, `ml`, `ml2`, `normed_in_S2`, `so3_closed_under_inverse`, `so3_invs_coe`, `split2`, `unitary_invs_coe`, `wopts`, `σ_def`, `τ_def`	16
Total	34

(root)

Definitions

Name	Category	Theorems
`FG2` 📖	CompOp	6 math math: `countable_of_fg2`, `to_sato_is_bijective`, `to_sato_range`, `to_sato_is_injective`, `to_sato_is_surjective`, `free_group_of_rank_two_is_self_paradoxical`
`MAT` 📖	CompOp	22 math math: `inv7lemma`, `COB_mat_is_ortho`, `rot_mat_inner_is_special`, `mtinv_lem2`, `M_s_normed_transpose_def`, `rot_mat_inner_comp_add`, `s_i_op_n_equiv`, `to_MAT_pow`, `msinv_lem2`, `to_MAT_mul`, `rot_mat_is_special`, `v2m_equiv`, `msinv_lem`, `M_t_normed_transpose_def`, `to_MAT_prod`, `t_i_op_n_equiv`, `mtinv_lem`, `M_t_normed_is_special`, `to_MAT_inj`, `M_s_normed_is_special`, `rot_mat_comp_add`, `diagonal_const_comm`
`R3` 📖	CompOp	77 math math: `countable_bad_skew_rot`, `spar_up_rot`, `s2_uncountable`, `orth_dim_3`, `same_char`, `spar_add`, `hmo_is_surjective`, `rot_iso_pow_lemma`, `orth_nonempty`, `hf`, `SO3_smul_def`, `COB_MB_is_ortho`, `x_axis_on_sphere`, `hausdorff_paradox`, `normed_in_S2`, `BadAtN_skew_rot_countable`, `COB_to_basis`, `srot_containment`, `orth_dim_2`, `so3_diff_lin`, `instSMulCommClassRealSubtypeMatrixFinOfNatNatMemSubmonoidSO3R3`, `spar_up_2`, `rot_iso_fixed_back`, `cob_mat_other_repr`, `rips_add`, `banach_tarski_paradox_B3`, `skew_rot_comp_add`, `operp_up_2`, `cone_lemma`, `so3_fixes_norm`, `rot_pow_lemma`, `isometry_of_so3`, `internal_pr`, `BadAtN_skew_rot`, `triv_rot_inner`, `fixed_lemma`, `triv_so3`, `triv_rot_by_parts`, `ih`, `R3_dim_3`, `lb_card_s2`, `banach_tarski_paradox_s2`, `origin_cont`, `rot_iso_comp_add`, `same_char_0`, `rot_comp_add`, `f_triv_g3`, `up_mem`, `SO3_G3_action_equiv`, `orth_toMatrix_mulVec_repr`, `K_id`, `triv_rot_iso`, `so3_fixes_s2`, `block_1_lem`, `dim_ker`, `same_action`, `inner_as_to_matrix_MB`, `bad_as_union_skew_rot`, `operp_add`, `hmo_is_bijective`, `same_mult`, `rot_containment_S2`, `spar_operp`, `inner_as_to_matrix`, `el_by_parts`, `operp_up`, `b3min_is_trunc_cone_s2`, `rot_iso_power_lemma`, `block_repr`, `SATO_smul_def`, `hmo_is_injective`, `banach_tarski_paradox_B3_minus_origin`, `rot_iso_comp`, `trunc_cone_sub_ball`, `skew_rot_power_lemma`, `operp_spar`, `block_2_lem`
`R3_raw` 📖	CompOp	—
`S2` 📖	CompOp	13 math math: `s2_uncountable`, `x_axis_on_sphere`, `hausdorff_paradox`, `normed_in_S2`, `cone_lemma`, `fixed_lemma`, `trunc_cone_lemma`, `ih`, `lb_card_s2`, `banach_tarski_paradox_s2`, `so3_fixes_s2`, `rot_containment_S2`, `b3min_is_trunc_cone_s2`
`SO3` 📖	CompOp	47 math math: `hmo_is_surjective`, `to_sato_is_bijective`, `s_i_op_n_equiv_2`, `so3_invs_coe`, `idlem`, `SO3_smul_def`, `to_sato_range`, `countable_bad_rots`, `hausdorff_paradox`, `s_mem`, `to_sato_is_injective`, `s_i_op_n_def`, `so3_diff_lin`, `rot_mat_inner_is_special`, `instSMulCommClassRealSubtypeMatrixFinOfNatNatMemSubmonoidSO3R3`, `rot_containment_general`, `bad_as_union_rot`, `S2_equidecomposible_of_S2_minus_countable`, `mapMatrix_is_map`, `s_i_op_n_equiv`, `t_i_op_n_def`, `triv_rot`, `so3_fixes_norm`, `to_sato_is_surjective`, `rot_pow_lemma`, `isometry_of_so3`, `rot_mat_is_special`, `fixed_lemma`, `triv_so3`, `banach_tarski_paradox_s2`, `t_mem`, `same_char_0`, `rot_comp_add`, `so3_cancel_lem`, `SO3_G3_action_equiv`, `t_i_op_n_equiv`, `so3_fixes_s2`, `same_action`, `M_t_normed_is_special`, `hmo_is_bijective`, `rot_containment_S2`, `M_s_normed_is_special`, `cast_root_mult1`, `t_i_op_n_equiv_2`, `SATO_smul_def`, `hmo_is_injective`, `banach_tarski_paradox_B3_minus_origin`
`SO3_action_on_MAT` 📖	CompOp	—
`SO3_action_on_R3` 📖	CompOp	13 math math: `countable_bad_rots`, `hausdorff_paradox`, `rot_containment_general`, `bad_as_union_rot`, `S2_equidecomposible_of_S2_minus_countable`, `rot_pow_lemma`, `isometry_of_so3`, `triv_so3`, `banach_tarski_paradox_s2`, `rot_comp_add`, `so3_fixes_s2`, `rot_containment_S2`, `banach_tarski_paradox_B3_minus_origin`
`chartype` 📖	CompOp	6 math math: `all_sinv_equiv`, `if_not_all_init_s_w`, `if_not_all_sinv_w`, `countable_chartype`, `finite_chartype`, `reduce_invRev_right_cancel`
`f` 📖	CompOp	9 math math: `collapse_iter`, `rot_pow_lemma`, `isometry_of_so3`, `triv_so3`, `rot_comp_add`, `f_triv_g3`, `so3_fixes_s2`, `rot_containment_S2`, `conj_bad_el`
`normed` 📖	CompOp	3 math math: `normed_in_S2`, `cone_lemma`, `trunc_cone_lemma`
`origin` 📖	CompOp	6 math math: `countable_bad_skew_rot`, `BadAtN_skew_rot_countable`, `srot_containment`, `BadAtN_skew_rot`, `origin_cont`, `bad_as_union_skew_rot`
`so3_has_inv` 📖	CompOp	—
`to_R3` 📖	CompOp	2 math math: `SO3_smul_def`, `SATO_smul_def`
`σ` 📖	CompOp	—
`σchar` 📖	CompOp	3 math math: `collapse_replics_1`, `σ_def`, `collapse_replics_2`
`τ` 📖	CompOp	—
`τchar` 📖	CompOp	1 math math: `τ_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`SO3_smul_def` 📖	mathematical	—	`SO3` `R3` `to_R3`	—	—
`countable_chartype` 📖	mathematical	—	`chartype`	—	`finite_chartype`
`countable_of_fg2` 📖	mathematical	—	`FG2`	—	`countable_chartype`
`fcomp` 📖	—	—	—	—	—
`finite_chartype` 📖	mathematical	—	`chartype`	—	—
`finj` 📖	—	—	—	—	—
`ml` 📖	—	—	—	—	—
`ml2` 📖	—	—	—	—	`ml`
`normed_in_S2` 📖	mathematical	—	`R3` `S2` `normed`	—	—
`so3_closed_under_inverse` 📖	—	`MAT` `SO3`	—	—	—
`so3_invs_coe` 📖	mathematical	—	`SO3`	—	—
`split2` 📖	—	—	—	—	—
`unitary_invs_coe` 📖	—	—	—	—	—
`wopts` 📖	—	—	—	—	—
`σ_def` 📖	mathematical	—	`σchar`	—	—
`τ_def` 📖	mathematical	—	`τchar`	—	—

---

← Back to Index