Theoremsantilipschitz, coeFn_injective, coe_comp, coe_id, coe_mul, coe_one, coe_toAffineMap, coe_toContinuousAffineMap, comp_assoc, comp_continuous_iff, comp_id, continuous, diam_image, diam_range, dist_map, ediam_image, ediam_range, edist_map, ext, ext_iff, id_apply, id_comp, id_toAffineMap, injective, isometry, linear_eq_linearIsometry, lipschitz, map_eq_iff, map_ne, map_vadd, map_vsub, nndist_map, norm_map, toAffineMap_injective, toContinuousAffineMap_id, toContinuousAffineMap_inj, toContinuousAffineMap_injective, antilipschitz, apply_symm_apply, bijective, coeFn_injective, coe_constVAdd, coe_constVSub, coe_inv, coe_mk, coe_mk', coe_mul, coe_ofEq_apply, coe_one, coe_refl, coe_symm_toAffineEquiv, coe_symm_toContinuousAffineEquiv, coe_symm_toHomeomorph, coe_symm_toIsometryEquiv, coe_symm_trans, coe_toAffineEquiv, coe_toAffineIsometry, coe_toContinuousAffineEquiv, coe_toHomeomorph, coe_toIsometryEquiv, coe_trans, coe_vaddConst, coe_vaddConst', coe_vaddConst_symm, comp_continuousOn_iff, comp_continuous_iff, constVAdd_zero, continuous, continuousAt, continuousOn, continuousWithinAt, diam_image, dist_map, dist_pointReflection_fixed, dist_pointReflection_self, dist_pointReflection_self', dist_pointReflection_self_real, ediam_image, edist_map, ext, ext_iff, injective, isometry, linearIsometryEquiv_mk', linear_eq_linear_isometry, lipschitz, map_eq_iff, map_ne, map_vadd, map_vsub, norm_map, ofEq_rfl, ofEq_symm, ofTop_apply, ofTop_symm_apply_coe, pointReflection_apply, pointReflection_fixed_iff, pointReflection_involutive, pointReflection_midpoint_left, pointReflection_midpoint_right, pointReflection_self, pointReflection_symm, pointReflection_toAffineEquiv, range_eq_univ, refl_trans, self_trans_symm, surjective, symm_apply_apply, symm_bijective, symm_constVSub, symm_symm, symm_trans_self, toAffineEquiv_injective, toAffineEquiv_refl, toAffineEquiv_symm, toContinuousAffineEquiv_inj, toContinuousAffineEquiv_injective, toContinuousAffineEquiv_refl, toContinuousAffineEquiv_symm, toHomeomorph_refl, toHomeomorph_symm, toIsometryEquiv_refl, toIsometryEquiv_symm, trans_assoc, trans_refl, vaddConst_toAffineEquiv, vadd_vsub, coe_subtypeₐᵢ, equivMapOfInjective_toFun, apply_symm_apply, coe_apply, toAffineMap_eq, linear_equivMapOfInjective, subtypeₐᵢ_linear, subtypeₐᵢ_linearIsometry, subtypeₐᵢ_toAffineMap, toContinuousAffineMap_subtypeₐᵢ, coe_toAffineIsometry, toAffineIsometry_linearIsometry, toAffineIsometry_toAffineMap, coe_toAffineIsometryEquiv, toAffineIsometryEquiv_linearIsometryEquiv, toAffineIsometryEquiv_toAffineEquiv, toAffineIsometryEquiv_toAffineIsometry | 144 |