ContinuousAffineMap

📁 Source: Mathlib/Topology/Algebra/ContinuousAffineMap.lean

Statistics

Metric	Count
Definitions `ContinuousAffineMap`, `comp`, `const`, `contLinear`, `decompAffineEquiv`, `decompEquiv`, `decompLinearEquiv`, `id`, `instAdd`, `instAddCommGroup`, `instAddTorsor`, `instCoeAffineMap`, `instCoeHeadContinuousMap`, `instDistribMulActionOfSMulCommClassOfContinuousConstSMul`, `instFunLike`, `instInhabited`, `instModuleOfSMulCommClassOfContinuousConstSMul`, `instMulAction`, `instNeg`, `instSMul`, `instSub`, `instZero`, `lineMap`, `prod`, `prodMap`, `toAffineMap`, `toContinuousMap`, `toContinuousAffineMap`, `«term_→ᴬ[_]_»`	29
Theorems `add_apply`, `add_contLinear`, `apply_lineMap`, `apply_lineMap'`, `coe_add`, `coe_comp`, `coe_const`, `coe_contLinear`, `coe_contLinear_eq_linear`, `coe_continuousMap_mk`, `coe_id`, `coe_injective`, `coe_lineMap_eq`, `coe_linear_eq_coe_contLinear`, `coe_mk`, `coe_mk_contLinear_eq_linear`, `coe_neg`, `coe_prod`, `coe_prodMap`, `coe_smul`, `coe_sub`, `coe_toAffineMap`, `coe_toAffineMap_mk`, `coe_to_continuousMap`, `coe_zero`, `comp_apply`, `comp_contLinear`, `comp_id`, `congr_fun`, `const_contLinear`, `cont`, `contLinear_eq_zero_iff_exists_const`, `contLinear_map_vsub`, `continuous`, `decomp`, `decompAffineEquiv_symm_apply`, `decompAffineEquiv_symm_contLinear`, `decompEquiv_symm_apply`, `decompEquiv_symm_contLinear`, `decompLinearEquiv_symm_apply`, `decompLinearEquiv_symm_contLinear`, `ext`, `ext_iff`, `fst_decompAffineEquiv`, `fst_decompEquiv`, `fst_decompLinearEquiv`, `id_comp`, `instContinuousMapClass`, `instIsCentralScalar`, `lineMap_apply'`, `lineMap_toAffineMap`, `linear_decompAffineEquiv`, `map_vadd`, `mk_coe`, `neg_apply`, `neg_contLinear`, `prodMap_apply`, `prodMap_contLinear`, `prodMap_toAffineMap`, `prod_apply`, `prod_contLinear`, `prod_toAffineMap`, `smul_apply`, `smul_contLinear`, `snd_decompAffineEquiv`, `snd_decompEquiv`, `snd_decompLinearEquiv`, `sub_apply`, `sub_contLinear`, `toAffineMap_injective`, `toContinuousMap_coe`, `toFun_eq_coe`, `to_continuousMap_injective`, `vadd_apply`, `vadd_contLinear`, `vadd_toAffineMap`, `vsub_apply`, `vsub_contLinear`, `vsub_toAffineMap`, `zero_apply`, `zero_contLinear`, `coe_toContinuousAffineMap`, `toContinuousAffineMap_contLinear`, `toContinuousAffineMap_map_zero`	84
Total	113

ContinuousAffineMap

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	8 math math: `comp_apply`, `id_comp`, `comp_contLinear`, `coe_comp`, `ContinuousAffineEquiv.trans_toContinuousAffineMap`, `norm_comp_le`, `signedDist_apply`, `comp_id`
`const` 📖	CompOp	5 math math: `const_contLinear`, `contLinear_eq_zero_iff_exists_const`, `coe_const`, `signedDist_linear_apply`, `signedDist_apply`
`contLinear` 📖	CompOp	40 math math: `neg_contLinear`, `fderiv`, `const_contLinear`, `EuclideanGeometry.orthogonalProjection_contLinear`, `HasFTaylorSeriesUpToOn.comp_continuousAffineMap`, `decomp`, `coe_mk_contLinear_eq_linear`, `smul_contLinear`, `norm_def`, `comp_contLinear`, `decompEquiv_symm_contLinear`, `decompLinearEquiv_symm_contLinear`, `coe_linear_eq_coe_contLinear`, `norm_eq`, `norm_contLinear_le`, `hasStrictFDerivAt`, `sub_contLinear`, `decompLinearIsometryEquiv_symm_contLinear`, `contLinear_eq_zero_iff_exists_const`, `coe_contLinear_eq_linear`, `prod_contLinear`, `map_vadd`, `prodMap_contLinear`, `add_contLinear`, `hasFDerivAtFilter`, `hasFDerivAt`, `snd_decompLinearIsometryEquiv`, `fderivWithin`, `vadd_contLinear`, `coe_contLinear`, `ContinuousLinearMap.toContinuousAffineMap_contLinear`, `snd_decompEquiv`, `contLinear_map_vsub`, `hasFDerivWithinAt`, `snd_decompLinearEquiv`, `snd_decompAffineEquiv`, `vsub_contLinear`, `decompAffineEquiv_symm_contLinear`, `zero_contLinear`, `toConstProdContinuousLinearMap_snd`
`decompAffineEquiv` 📖	CompOp	5 math math: `fst_decompAffineEquiv`, `linear_decompAffineEquiv`, `decompAffineEquiv_symm_apply`, `snd_decompAffineEquiv`, `decompAffineEquiv_symm_contLinear`
`decompEquiv` 📖	CompOp	4 math math: `fst_decompEquiv`, `decompEquiv_symm_contLinear`, `decompEquiv_symm_apply`, `snd_decompEquiv`
`decompLinearEquiv` 📖	CompOp	5 math math: `fst_decompLinearEquiv`, `decompLinearEquiv_symm_contLinear`, `linear_decompAffineEquiv`, `decompLinearEquiv_symm_apply`, `snd_decompLinearEquiv`
`id` 📖	CompOp	5 math math: `id_comp`, `AffineIsometry.toContinuousAffineMap_id`, `coe_id`, `signedDist_apply`, `comp_id`
`instAdd` 📖	CompOp	3 math math: `coe_add`, `add_apply`, `add_contLinear`
`instAddCommGroup` 📖	CompOp	55 math math: `lineMap_apply'`, `fst_decompLinearEquiv`, `signedDist_right_congr`, `signedDist_left_congr`, `signedDist_triangle`, `signedDist_linear_apply_apply`, `signedDist_le_dist`, `signedDist_apply_apply`, `decompLinearEquiv_symm_contLinear`, `vadd_toAffineMap`, `signedDist_eq_zero_of_orthogonal`, `AffineSubspace.signedInfDist_eq_signedDist_of_mem`, `signedDist_zero`, `AffineSubspace.signedInfDist_eq_signedDist_orthogonalProjection`, `fst_decompAffineEquiv`, `signedDist_triangle_left`, `signedDist_smul_of_pos`, `signedDist_lineMap_lineMap`, `linear_decompAffineEquiv`, `signedDist_vadd_left_swap`, `signedDist_vadd_right`, `signedDist_lineMap_left`, `signedDist_anticomm`, `decompAffineEquiv_symm_apply`, `signedDist_triangle_right`, `abs_signedDist_eq_dist_iff_vsub_mem_span`, `signedDist_neg`, `signedDist_vsub_self_rev`, `signedDist_linear_apply`, `signedDist_self`, `signedDist_vsub_self`, `signedDist_smul`, `signedDist_smul_of_neg`, `signedDist_vadd_right_swap`, `vadd_contLinear`, `signedDist_vadd_left`, `signedDist_apply_linear_apply`, `AffineSubspace.signedInfDist_singleton`, `decompLinearEquiv_symm_apply`, `signedDist_right_lineMap`, `vsub_toAffineMap`, `AffineSubspace.signedInfDist_def`, `signedDist_lineMap_right`, `vsub_apply`, `signedDist_apply`, `signedDist_eq_dist_iff_vsub_mem_span`, `snd_decompLinearEquiv`, `snd_decompAffineEquiv`, `vsub_contLinear`, `decompAffineEquiv_symm_contLinear`, `abs_signedDist_le_dist`, `signedDist_apply_linear`, `signedDist_left_lineMap`, `signedDist_vadd_vadd`, `vadd_apply`
`instAddTorsor` 📖	CompOp	51 math math: `lineMap_apply'`, `signedDist_right_congr`, `signedDist_left_congr`, `signedDist_triangle`, `signedDist_linear_apply_apply`, `signedDist_le_dist`, `signedDist_apply_apply`, `vadd_toAffineMap`, `signedDist_eq_zero_of_orthogonal`, `AffineSubspace.signedInfDist_eq_signedDist_of_mem`, `signedDist_zero`, `AffineSubspace.signedInfDist_eq_signedDist_orthogonalProjection`, `fst_decompAffineEquiv`, `signedDist_triangle_left`, `signedDist_smul_of_pos`, `signedDist_lineMap_lineMap`, `linear_decompAffineEquiv`, `signedDist_vadd_left_swap`, `signedDist_vadd_right`, `signedDist_lineMap_left`, `signedDist_anticomm`, `decompAffineEquiv_symm_apply`, `signedDist_triangle_right`, `abs_signedDist_eq_dist_iff_vsub_mem_span`, `signedDist_neg`, `signedDist_vsub_self_rev`, `signedDist_linear_apply`, `signedDist_self`, `signedDist_vsub_self`, `signedDist_smul`, `signedDist_smul_of_neg`, `signedDist_vadd_right_swap`, `vadd_contLinear`, `signedDist_vadd_left`, `signedDist_apply_linear_apply`, `AffineSubspace.signedInfDist_singleton`, `signedDist_right_lineMap`, `vsub_toAffineMap`, `AffineSubspace.signedInfDist_def`, `signedDist_lineMap_right`, `vsub_apply`, `signedDist_apply`, `signedDist_eq_dist_iff_vsub_mem_span`, `snd_decompAffineEquiv`, `vsub_contLinear`, `decompAffineEquiv_symm_contLinear`, `abs_signedDist_le_dist`, `signedDist_apply_linear`, `signedDist_left_lineMap`, `signedDist_vadd_vadd`, `vadd_apply`
`instCoeAffineMap` 📖	CompOp	—
`instCoeHeadContinuousMap` 📖	CompOp	—
`instDistribMulActionOfSMulCommClassOfContinuousConstSMul` 📖	CompOp	—
`instFunLike` 📖	CompOp	191 math math: `Affine.Simplex.orthogonalProjectionSpan_map`, `EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal`, `lineMap_apply'`, `fderiv`, `differentiableWithinAt`, `fst_decompLinearEquiv`, `ext_iff`, `Affine.Simplex.orthogonalProjection_vadd_smul_vsub_orthogonalProjection`, `comp_apply`, `prodMap_apply`, `coe_mk`, `EuclideanGeometry.orthogonalProjection_congr`, `neg_apply`, `toFun_eq_coe`, `ContinuousAffineEquiv.coe_toContinuousAffineMap`, `coe_sub`, `differentiable`, `smul_apply`, `EuclideanGeometry.dist_orthogonalProjection_eq_iff_oangle_eq`, `lintegral_fderiv_lineMap_eq_edist`, `AffineSubspace.coe_subtypeA`, `signedDist_right_congr`, `Affine.Simplex.sign_signedInfDist_lineMap_incenter_touchpoint`, `fst_decompEquiv`, `coe_to_continuousMap`, `HasFTaylorSeriesUpToOn.comp_continuousAffineMap`, `coe_lineMap_eq`, `EuclideanGeometry.reflection_vadd_smul_vsub_orthogonalProjection`, `EuclideanGeometry.inter_eq_singleton_orthogonalProjection`, `signedDist_triangle`, `Affine.Simplex.orthogonalProjectionSpan_eq_point`, `signedDist_linear_apply_apply`, `decomp`, `zero_apply`, `EuclideanGeometry.orthogonalProjection_map`, `EuclideanGeometry.angle_orthogonalProjection_self`, `ContinuousLinearMap.toContinuousAffineMap_map_zero`, `EuclideanGeometry.orthogonalProjection_apply_mem`, `EuclideanGeometry.dist_orthogonalProjection_eq_of_oangle_eq`, `norm_def`, `signedDist_le_dist`, `EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq`, `signedDist_apply_apply`, `EuclideanGeometry.dist_orthogonalProjection_eq_of_two_zsmul_oangle_eq`, `EuclideanGeometry.orthogonalProjection_apply'`, `Affine.Simplex.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq`, `decompLinearIsometryEquiv_symm_apply`, `EuclideanGeometry.orthogonalProjection_orthogonalProjection_of_le`, `EuclideanGeometry.Sphere.isTangent_iff_isTangentAt_orthogonalProjection`, `Affine.Simplex.ExcenterExists.sign_signedInfDist_touchpoint`, `coe_add`, `signedDist_eq_zero_of_orthogonal`, `coe_toAffineMap`, `AffineSubspace.signedInfDist_eq_signedDist_of_mem`, `Affine.Simplex.signedInfDist_apply_self`, `coe_injective`, `signedDist_zero`, `AffineSubspace.signedInfDist_eq_signedDist_orthogonalProjection`, `Affine.Simplex.orthogonalProjectionSpan_congr`, `fst_decompAffineEquiv`, `signedDist_triangle_left`, `coe_comp`, `EuclideanGeometry.Sphere.orthogonalProjection_orthRadius_center`, `hasStrictFDerivAt`, `EuclideanGeometry.orthogonalProjection_subtype`, `EuclideanGeometry.two_zsmul_oangle_self_orthogonalProjection`, `Affine.Simplex.ExcenterExists.sign_signedInfDist_lineMap_excenter_touchpoint`, `contDiff`, `EuclideanGeometry.orthogonalProjection_vadd_eq_self`, `toContinuousMap_coe`, `decompEquiv_symm_apply`, `signedDist_smul_of_pos`, `EuclideanGeometry.oangle_orthogonalProjection_self`, `apply_lineMap'`, `signedDist_lineMap_lineMap`, `EuclideanGeometry.dist_orthogonalProjection_eq_dist_iff_eq_of_mem`, `AffineSubspace.abs_signedInfDist_eq_dist_of_mem_affineSpan_insert`, `signedDist_vadd_left_swap`, `Affine.Simplex.orthogonalProjection_circumcenter`, `Affine.Simplex.exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter`, `instContinuousMapClass`, `signedDist_vadd_right`, `Affine.Simplex.orthogonalProjection_eq_circumcenter_of_exists_dist_eq`, `EuclideanGeometry.oangle_eq_of_dist_orthogonalProjection_eq`, `map_vadd`, `EuclideanGeometry.orthogonalProjection_affineSpan_singleton`, `signedDist_lineMap_left`, `coe_const`, `EuclideanGeometry.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq`, `coe_zero`, `signedDist_anticomm`, `add_apply`, `coe_id`, `decompAffineEquiv_symm_apply`, `EuclideanGeometry.orthogonalProjection_vadd_smul_vsub_orthogonalProjection`, `signedDist_triangle_right`, `Affine.Simplex.orthogonalProjectionSpan_faceOpposite_eq_point_rev`, `EuclideanGeometry.dist_orthogonalProjection_eq_infNndist`, `abs_signedDist_eq_dist_iff_vsub_mem_span`, `signedDist_neg`, `signedDist_vsub_self_rev`, `EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangent`, `coe_smul`, `EuclideanGeometry.orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem`, `congr_fun`, `signedDist_self`, `hasFDerivAtFilter`, `signedDist_vsub_self`, `Affine.Simplex.exists_forall_signedInfDist_eq_iff_eq_incenter`, `signedDist_smul`, `EuclideanGeometry.dist_eq_iff_dist_orthogonalProjection_eq`, `hasFDerivAt`, `norm_image_zero_le`, `apply_lineMap`, `EuclideanGeometry.dist_orthogonalProjection_eq_infDist`, `EuclideanGeometry.orthogonalProjection_mem`, `Affine.Simplex.orthogonalProjectionSpan_restrict`, `signedDist_smul_of_neg`, `EuclideanGeometry.dist_orthogonalProjection_eq_zero_iff`, `Affine.Simplex.sign_signedInfDist_touchpoint_empty`, `signedDist_vadd_right_swap`, `fderivWithin`, `EuclideanGeometry.exists_dist_eq_iff_exists_dist_orthogonalProjection_eq`, `EuclideanGeometry.Sphere.IsTangentAt.eq_orthogonalProjection`, `sub_apply`, `EuclideanGeometry.reflection_eq_iff_orthogonalProjection_eq`, `EuclideanGeometry.orthogonalProjection_orthogonalProjection`, `EuclideanGeometry.orthogonalProjection_vsub_mem_direction`, `signedDist_vadd_left`, `Affine.Simplex.orthogonalProjection_eq_circumcenter_of_dist_eq`, `EuclideanGeometry.vsub_orthogonalProjection_mem_direction`, `Affine.Simplex.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection`, `decompLinearEquiv_symm_apply`, `EuclideanGeometry.Sphere.IsTangent.isTangentAt`, `contLinear_map_vsub`, `EuclideanGeometry.reflection_apply'`, `surjOn_extremePoints_image`, `differentiableOn`, `coe_continuousMap_mk`, `EuclideanGeometry.oangle_self_orthogonalProjection`, `norm_comp_le`, `signedDist_right_lineMap`, `Affine.Simplex.abs_signedInfDist_eq_dist_of_mem_affineSpan_range`, `Affine.Simplex.ExcenterExists.signedInfDist_excenter`, `Affine.Simplex.orthogonalProjectionSpan_reindex`, `AffineSubspace.signedInfDist_def`, `prod_apply`, `signedDist_lineMap_right`, `Affine.Simplex.orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle`, `fst_decompLinearIsometryEquiv`, `vsub_apply`, `Affine.Simplex.sign_signedInfDist_incenter`, `Affine.Simplex.ExcenterExists.sign_signedInfDist_excenter`, `hasFDerivWithinAt`, `Affine.Simplex.signedInfDist_affineCombination`, `EuclideanGeometry.angle_self_orthogonalProjection`, `signedDist_eq_dist_iff_vsub_mem_span`, `EuclideanGeometry.orthogonalProjection_eq_self_iff`, `Affine.Simplex.ExcenterExists.signedInfDist_excenter_eq_mul_sum_inv`, `EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal`, `Affine.Simplex.exists_forall_signedInfDist_eq_iff_excenterExists_and_eq_excenter`, `EuclideanGeometry.eq_orthogonalProjection_of_eq_subspace`, `EuclideanGeometry.orthogonalProjection_apply`, `AffineSubspace.signedInfDist_apply_self`, `EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection`, `EuclideanGeometry.orthogonalProjection_mem_orthogonal`, `toConstProdContinuousLinearMap_fst`, `EuclideanGeometry.two_zsmul_oangle_orthogonalProjection_self`, `abs_signedDist_le_dist`, `AffineSubspace.signedInfDist_apply_of_mem`, `EuclideanGeometry.orthogonalProjection_sup_of_orthogonalProjection_eq`, `EuclideanGeometry.coe_orthogonalProjection_eq_iff_mem`, `ContinuousLinearMap.coe_toContinuousAffineMap`, `continuous`, `Affine.Simplex.signedInfDist_apply_of_ne`, `AffineIsometry.coe_toContinuousAffineMap`, `signedDist_left_lineMap`, `coe_neg`, `EuclideanGeometry.dist_orthogonalProjection_line_eq_iff_two_zsmul_oangle_eq`, `EuclideanGeometry.orthogonalProjection_eq_iff_mem`, `EuclideanGeometry.dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq`, `differentiableAt`, `coe_prod`, `coe_prodMap`, `EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt`, `EuclideanGeometry.dist_set_eq_iff_dist_orthogonalProjection_eq`, `signedDist_vadd_vadd`, `vadd_apply`, `EuclideanGeometry.orthogonalProjection_mem_subspace_eq_self`, `Affine.Triangle.dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq`, `Affine.Simplex.signedInfDist_incenter`
`instInhabited` 📖	CompOp	—
`instModuleOfSMulCommClassOfContinuousConstSMul` 📖	CompOp	55 math math: `lineMap_apply'`, `fst_decompLinearEquiv`, `signedDist_right_congr`, `signedDist_left_congr`, `signedDist_triangle`, `signedDist_linear_apply_apply`, `signedDist_le_dist`, `signedDist_apply_apply`, `decompLinearEquiv_symm_contLinear`, `decompLinearIsometryEquiv_symm_apply`, `signedDist_eq_zero_of_orthogonal`, `AffineSubspace.signedInfDist_eq_signedDist_of_mem`, `signedDist_zero`, `AffineSubspace.signedInfDist_eq_signedDist_orthogonalProjection`, `fst_decompAffineEquiv`, `signedDist_triangle_left`, `decompLinearIsometryEquiv_symm_contLinear`, `signedDist_smul_of_pos`, `signedDist_lineMap_lineMap`, `linear_decompAffineEquiv`, `signedDist_vadd_left_swap`, `signedDist_vadd_right`, `signedDist_lineMap_left`, `signedDist_anticomm`, `decompAffineEquiv_symm_apply`, `signedDist_triangle_right`, `abs_signedDist_eq_dist_iff_vsub_mem_span`, `signedDist_neg`, `signedDist_vsub_self_rev`, `signedDist_linear_apply`, `signedDist_self`, `signedDist_vsub_self`, `signedDist_smul`, `snd_decompLinearIsometryEquiv`, `signedDist_smul_of_neg`, `signedDist_vadd_right_swap`, `signedDist_vadd_left`, `signedDist_apply_linear_apply`, `AffineSubspace.signedInfDist_singleton`, `decompLinearEquiv_symm_apply`, `signedDist_right_lineMap`, `AffineSubspace.signedInfDist_def`, `signedDist_lineMap_right`, `fst_decompLinearIsometryEquiv`, `signedDist_apply`, `signedDist_eq_dist_iff_vsub_mem_span`, `snd_decompLinearEquiv`, `snd_decompAffineEquiv`, `decompAffineEquiv_symm_contLinear`, `toConstProdContinuousLinearMap_fst`, `abs_signedDist_le_dist`, `signedDist_apply_linear`, `signedDist_left_lineMap`, `signedDist_vadd_vadd`, `toConstProdContinuousLinearMap_snd`
`instMulAction` 📖	CompOp	—
`instNeg` 📖	CompOp	3 math math: `neg_contLinear`, `neg_apply`, `coe_neg`
`instSMul` 📖	CompOp	4 math math: `smul_apply`, `smul_contLinear`, `coe_smul`, `instIsCentralScalar`
`instSub` 📖	CompOp	3 math math: `coe_sub`, `sub_contLinear`, `sub_apply`
`instZero` 📖	CompOp	3 math math: `zero_apply`, `coe_zero`, `zero_contLinear`
`lineMap` 📖	CompOp	4 math math: `lintegral_fderiv_lineMap_eq_edist`, `coe_lineMap_eq`, `lineMap_toAffineMap`, `apply_lineMap'`
`prod` 📖	CompOp	4 math math: `prod_contLinear`, `prod_apply`, `prod_toAffineMap`, `coe_prod`
`prodMap` 📖	CompOp	5 math math: `prodMap_apply`, `ContinuousAffineEquiv.prodCongr_toContinuousAffineMap`, `prodMap_toAffineMap`, `prodMap_contLinear`, `coe_prodMap`
`toAffineMap` 📖	CompOp	19 math math: `toFun_eq_coe`, `mk_coe`, `prodMap_toAffineMap`, `lineMap_toAffineMap`, `vadd_toAffineMap`, `coe_linear_eq_coe_contLinear`, `coe_toAffineMap`, `AffineSubspace.signedInfDist_eq_const_of_mem`, `AffineSubspace.subtypeA_toAffineMap`, `coe_contLinear_eq_linear`, `coe_contLinear`, `signedDist_apply_linear_apply`, `vsub_toAffineMap`, `EuclideanGeometry.orthogonalProjection_linear`, `prod_toAffineMap`, `signedDist_apply_linear`, `ContinuousAffineEquiv.toContinuousAffineMap_toAffineMap`, `coe_toAffineMap_mk`, `cont`
`toContinuousMap` 📖	CompOp	2 math math: `toContinuousMap_coe`, `ContinuousAffineEquiv.toContinuousAffineMap_toContinuousMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instFunLike` `instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	—
`add_contLinear` 📖	mathematical	—	`contLinear` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instIsTopologicalAddTorsor` `ContinuousAffineMap` `instAdd` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.add` `IsTopologicalAddGroup.toContinuousAdd`	—	`instIsTopologicalAddTorsor`
`apply_lineMap` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `instFunLike` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap`	—	`coe_toAffineMap` `AffineMap.apply_lineMap`
`apply_lineMap'` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `instFunLike` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `lineMap`	—	`apply_lineMap`
`coe_add` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instFunLike` `instAdd` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	—
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `instFunLike` `comp`	—	—
`coe_const` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `instFunLike` `const`	—	—
`coe_contLinear` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `contLinear` `LinearMap` `LinearMap.instFunLike` `AffineMap.linear` `toAffineMap`	—	—
`coe_contLinear_eq_linear` 📖	mathematical	—	`ContinuousLinearMap.toLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `contLinear` `AffineMap.linear` `toAffineMap`	—	—
`coe_continuousMap_mk` 📖	mathematical	`Continuous` `AffineMap.toFun`	`toContinuousMap` `ContinuousAffineMap` `instFunLike` `instContinuousMapClass` `DFunLike.coe` `AffineMap` `AffineMap.instFunLike`	—	`instContinuousMapClass`
`coe_id` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `instFunLike` `id`	—	—
`coe_injective` 📖	mathematical	—	`ContinuousAffineMap` `DFunLike.coe` `instFunLike`	—	`DFunLike.coe_injective`
`coe_lineMap_eq` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `instFunLike` `lineMap` `AffineMap` `AffineMap.instFunLike` `AffineMap.lineMap`	—	—
`coe_linear_eq_coe_contLinear` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `AffineMap.linear` `toAffineMap` `ContinuousLinearMap` `ContinuousLinearMap.funLike` `contLinear`	—	—
`coe_mk` 📖	mathematical	`Continuous` `AffineMap.toFun`	`DFunLike.coe` `ContinuousAffineMap` `instFunLike` `AffineMap` `AffineMap.instFunLike`	—	—
`coe_mk_contLinear_eq_linear` 📖	mathematical	`Continuous` `AffineMap.toFun`	`DFunLike.coe` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `contLinear` `LinearMap` `LinearMap.instFunLike` `AffineMap.linear`	—	—
`coe_neg` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instFunLike` `instNeg` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`coe_prod` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instTopologicalSpaceProd` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `instFunLike` `prod` `Pi.prod`	—	—
`coe_prodMap` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instTopologicalSpaceProd` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `instFunLike` `prodMap`	—	—
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instFunLike` `instSMul` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	—
`coe_sub` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instFunLike` `instSub` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	—
`coe_toAffineMap` 📖	mathematical	—	`DFunLike.coe` `AffineMap` `AffineMap.instFunLike` `toAffineMap` `ContinuousAffineMap` `instFunLike`	—	—
`coe_toAffineMap_mk` 📖	mathematical	`Continuous` `AffineMap.toFun`	`toAffineMap`	—	—
`coe_to_continuousMap` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `toContinuousMap` `ContinuousAffineMap` `instFunLike` `instContinuousMapClass`	—	`instContinuousMapClass`
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instFunLike` `instZero` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `instFunLike` `comp`	—	—
`comp_contLinear` 📖	mathematical	—	`contLinear` `comp` `ContinuousLinearMap.comp` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `RingHomCompTriple.ids`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	`ext`
`congr_fun` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `instFunLike`	—	`DFunLike.congr_fun`
`const_contLinear` 📖	mathematical	—	`contLinear` `const` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.zero`	—	—
`cont` 📖	mathematical	—	`Continuous` `AffineMap.toFun` `toAffineMap`	—	—
`contLinear_eq_zero_iff_exists_const` 📖	mathematical	—	`contLinear` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.zero` `const`	—	`LinearMap.ext` `coe_contLinear_eq_linear` `ContinuousLinearMap.ext` `coe_linear_eq_coe_contLinear` `AffineMap.ext` `ext` `coe_toAffineMap` `AffineMap.const_apply` `coe_const` `AffineMap.linear_eq_zero_iff_exists_const`
`contLinear_map_vsub` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `contLinear` `VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup` `ContinuousAffineMap` `instFunLike`	—	`AffineMap.linearMap_vsub`
`continuous` 📖	mathematical	—	`Continuous` `DFunLike.coe` `ContinuousAffineMap` `instFunLike`	—	`cont`
`decomp` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instFunLike` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike` `contLinear` `instIsTopologicalAddTorsor` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`instIsTopologicalAddTorsor` `coe_mk_contLinear_eq_linear` `AffineMap.decomp` `Pi.add_apply` `LinearMap.map_zero` `zero_add` `Function.const_def`
`decompAffineEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instFunLike` `AffineEquiv` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Prod.instAddCommGroup` `ContinuousLinearMap.addCommGroup` `instAddCommGroup` `Prod.instModule` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `ContinuousLinearMap.module` `instModuleOfSMulCommClassOfContinuousConstSMul` `Prod.instAddTorsor` `instAddTorsor` `EquivLike.toFunLike` `AffineEquiv.equivLike` `AffineEquiv.symm` `decompAffineEquiv` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `ContinuousLinearMap.funLike`	—	`IsTopologicalAddGroup.toContinuousAdd`
`decompAffineEquiv_symm_contLinear` 📖	mathematical	—	`contLinear` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instIsTopologicalAddTorsor` `DFunLike.coe` `AffineEquiv` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousAffineMap` `Prod.instAddCommGroup` `ContinuousLinearMap.addCommGroup` `instAddCommGroup` `Prod.instModule` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `ContinuousLinearMap.module` `instModuleOfSMulCommClassOfContinuousConstSMul` `Prod.instAddTorsor` `instAddTorsor` `EquivLike.toFunLike` `AffineEquiv.equivLike` `AffineEquiv.symm` `decompAffineEquiv`	—	`instIsTopologicalAddTorsor` `IsTopologicalAddGroup.toContinuousAdd` `decompAffineEquiv.eq_1` `AffineEquiv.coe_symm_toEquiv` `decompEquiv_symm_contLinear`
`decompEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instFunLike` `Equiv` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `decompEquiv` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `ContinuousLinearMap.funLike`	—	—
`decompEquiv_symm_contLinear` 📖	mathematical	—	`contLinear` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instIsTopologicalAddTorsor` `DFunLike.coe` `Equiv` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousAffineMap` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `decompEquiv`	—	`ContinuousLinearMap.ext` `instIsTopologicalAddTorsor` `add_zero` `IsTopologicalAddTorsor.to_isTopologicalAddGroup`
`decompLinearEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instFunLike` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ContinuousLinearMap` `AddCommGroup.toAddCommMonoid` `Prod.instAddCommMonoid` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `instAddCommGroup` `Prod.instModule` `ContinuousLinearMap.module` `instModuleOfSMulCommClassOfContinuousConstSMul` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `decompLinearEquiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ContinuousLinearMap.funLike`	—	`RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousAdd`
`decompLinearEquiv_symm_contLinear` 📖	mathematical	—	`contLinear` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instIsTopologicalAddTorsor` `DFunLike.coe` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ContinuousLinearMap` `AddCommGroup.toAddCommMonoid` `ContinuousAffineMap` `Prod.instAddCommMonoid` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `instAddCommGroup` `Prod.instModule` `ContinuousLinearMap.module` `instModuleOfSMulCommClassOfContinuousConstSMul` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `decompLinearEquiv`	—	`ContinuousLinearMap.ext` `instIsTopologicalAddTorsor` `RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousAdd` `decompEquiv_symm_contLinear`
`ext` 📖	—	`DFunLike.coe` `ContinuousAffineMap` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `instFunLike`	—	`ext`
`fst_decompAffineEquiv` 📖	mathematical	—	`ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `AffineEquiv` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instAddCommGroup` `Prod.instAddCommGroup` `ContinuousLinearMap.addCommGroup` `instModuleOfSMulCommClassOfContinuousConstSMul` `Prod.instModule` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `ContinuousLinearMap.module` `instAddTorsor` `Prod.instAddTorsor` `EquivLike.toFunLike` `AffineEquiv.equivLike` `decompAffineEquiv` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`IsTopologicalAddGroup.toContinuousAdd`
`fst_decompEquiv` 📖	mathematical	—	`ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `Equiv` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompEquiv` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`fst_decompLinearEquiv` 📖	mathematical	—	`ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `LinearEquiv` `RingHomInvPair.ids` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instAddCommGroup` `Prod.instAddCommMonoid` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `instModuleOfSMulCommClassOfContinuousConstSMul` `Prod.instModule` `ContinuousLinearMap.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `decompLinearEquiv` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousAdd`
`id_comp` 📖	mathematical	—	`comp` `id`	—	`ext`
`instContinuousMapClass` 📖	mathematical	—	`ContinuousMapClass` `ContinuousAffineMap` `instFunLike`	—	`cont`
`instIsCentralScalar` 📖	mathematical	—	`IsCentralScalar` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instSMul` `MulOpposite` `MulOpposite.instMonoid` `SMulCommClass.op_right` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `ContinuousConstSMul.op`	—	`SMulCommClass.op_right` `ContinuousConstSMul.op` `ext` `IsCentralScalar.op_smul_eq_smul`
`lineMap_apply'` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `instFunLike` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `instAddCommGroup` `instModuleOfSMulCommClassOfContinuousConstSMul` `instAddTorsor` `AffineMap.instFunLike` `AffineMap.lineMap`	—	—
`lineMap_toAffineMap` 📖	mathematical	—	`toAffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `lineMap` `AffineMap.lineMap`	—	—
`linear_decompAffineEquiv` 📖	mathematical	—	`AffineEquiv.linear` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `Prod.instAddCommGroup` `ContinuousLinearMap.addCommGroup` `instModuleOfSMulCommClassOfContinuousConstSMul` `Prod.instModule` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `ContinuousLinearMap.module` `instAddTorsor` `Prod.instAddTorsor` `decompAffineEquiv` `decompLinearEquiv`	—	`RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousAdd`
`map_vadd` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `instFunLike` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `contLinear`	—	`AffineMap.map_vadd'`
`mk_coe` 📖	mathematical	`Continuous` `AffineMap.toFun` `toAffineMap`	`toAffineMap`	—	`ext`
`neg_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instFunLike` `instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`neg_contLinear` 📖	mathematical	—	`contLinear` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instIsTopologicalAddTorsor` `ContinuousAffineMap` `instNeg` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.neg`	—	`instIsTopologicalAddTorsor`
`prodMap_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instTopologicalSpaceProd` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `instFunLike` `prodMap`	—	—
`prodMap_contLinear` 📖	mathematical	—	`contLinear` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instTopologicalSpaceProd` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `instIsTopologicalAddTorsorProd` `prodMap` `ContinuousLinearMap.prodMap`	—	`instIsTopologicalAddTorsorProd`
`prodMap_toAffineMap` 📖	mathematical	—	`toAffineMap` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instTopologicalSpaceProd` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `prodMap` `AffineMap.prodMap`	—	—
`prod_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instTopologicalSpaceProd` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `instFunLike` `prod`	—	—
`prod_contLinear` 📖	mathematical	—	`contLinear` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instTopologicalSpaceProd` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `instIsTopologicalAddTorsorProd` `prod` `ContinuousLinearMap.prod`	—	`instIsTopologicalAddTorsorProd`
`prod_toAffineMap` 📖	mathematical	—	`toAffineMap` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instTopologicalSpaceProd` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `prod` `AffineMap.prod`	—	—
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instFunLike` `instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	—
`smul_contLinear` 📖	mathematical	—	`contLinear` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instIsTopologicalAddTorsor` `ContinuousAffineMap` `instSMul` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.instSMul` `DistribMulAction.toDistribSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`instIsTopologicalAddTorsor`
`snd_decompAffineEquiv` 📖	mathematical	—	`ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `AffineEquiv` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instAddCommGroup` `Prod.instAddCommGroup` `ContinuousLinearMap.addCommGroup` `instModuleOfSMulCommClassOfContinuousConstSMul` `Prod.instModule` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `ContinuousLinearMap.module` `instAddTorsor` `Prod.instAddTorsor` `EquivLike.toFunLike` `AffineEquiv.equivLike` `decompAffineEquiv` `contLinear` `instIsTopologicalAddTorsor`	—	`IsTopologicalAddGroup.toContinuousAdd`
`snd_decompEquiv` 📖	mathematical	—	`ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `Equiv` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `EquivLike.toFunLike` `Equiv.instEquivLike` `decompEquiv` `contLinear` `instIsTopologicalAddTorsor`	—	—
`snd_decompLinearEquiv` 📖	mathematical	—	`ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `LinearEquiv` `RingHomInvPair.ids` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instAddCommGroup` `Prod.instAddCommMonoid` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `instModuleOfSMulCommClassOfContinuousConstSMul` `Prod.instModule` `ContinuousLinearMap.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `decompLinearEquiv` `contLinear` `instIsTopologicalAddTorsor`	—	`RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousAdd`
`sub_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instFunLike` `instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	—
`sub_contLinear` 📖	mathematical	—	`contLinear` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instIsTopologicalAddTorsor` `ContinuousAffineMap` `instSub` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.sub`	—	`instIsTopologicalAddTorsor`
`toAffineMap_injective` 📖	—	`toAffineMap`	—	—	—
`toContinuousMap_coe` 📖	mathematical	—	`toContinuousMap` `toContinuousMap` `ContinuousAffineMap` `instFunLike` `instContinuousMapClass`	—	—
`toFun_eq_coe` 📖	mathematical	—	`AffineMap.toFun` `toAffineMap` `DFunLike.coe` `ContinuousAffineMap` `instFunLike`	—	—
`to_continuousMap_injective` 📖	—	`toContinuousMap` `ContinuousAffineMap` `instFunLike` `instContinuousMapClass`	—	—	`instContinuousMapClass` `ext` `ContinuousMap.congr_fun`
`vadd_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `instFunLike` `HVAdd.hVAdd` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instAddCommGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `instAddTorsor`	—	—
`vadd_contLinear` 📖	mathematical	—	`contLinear` `HVAdd.hVAdd` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instAddCommGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `instAddTorsor` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.add` `IsTopologicalAddGroup.toContinuousAdd` `instIsTopologicalAddTorsor`	—	—
`vadd_toAffineMap` 📖	mathematical	—	`toAffineMap` `HVAdd.hVAdd` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instAddCommGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `instAddTorsor` `AffineMap` `AffineMap.instAddCommGroup` `AffineMap.instAddTorsor`	—	—
`vsub_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instFunLike` `VSub.vsub` `AddTorsor.toVSub` `instAddCommGroup` `instAddTorsor`	—	—
`vsub_contLinear` 📖	mathematical	—	`contLinear` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instIsTopologicalAddTorsor` `VSub.vsub` `ContinuousAffineMap` `AddTorsor.toVSub` `instAddCommGroup` `instAddTorsor` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.sub`	—	`instIsTopologicalAddTorsor`
`vsub_toAffineMap` 📖	mathematical	—	`toAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `VSub.vsub` `ContinuousAffineMap` `AddTorsor.toVSub` `instAddCommGroup` `instAddTorsor` `AffineMap` `AffineMap.instAddCommGroup` `AffineMap.instAddTorsor`	—	—
`zero_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instFunLike` `instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`zero_contLinear` 📖	mathematical	—	`contLinear` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instIsTopologicalAddTorsor` `ContinuousAffineMap` `instZero` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.zero`	—	`instIsTopologicalAddTorsor`

ContinuousLinearMap

Definitions

Name	Category	Theorems
`toContinuousAffineMap` 📖	CompOp	5 math math: `toContinuousAffineMap_map_zero`, `ContinuousLinearEquiv.toContinuousAffineEquiv_toContinuousAffineMap`, `toContinuousAffineMap_contLinear`, `signedDist_apply`, `coe_toContinuousAffineMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toContinuousAffineMap` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instFunLike` `toContinuousAffineMap` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `funLike`	—	—
`toContinuousAffineMap_contLinear` 📖	mathematical	—	`ContinuousAffineMap.contLinear` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instIsTopologicalAddTorsor` `toContinuousAffineMap`	—	`instIsTopologicalAddTorsor`
`toContinuousAffineMap_map_zero` 📖	mathematical	—	`DFunLike.coe` `ContinuousAffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineMap.instFunLike` `toContinuousAffineMap` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `continuousSemilinearMapClass`

(root)

Definitions

Name	Category	Theorems
`ContinuousAffineMap` 📖	CompData	221 math math: `Affine.Simplex.orthogonalProjectionSpan_map`, `EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal`, `ContinuousAffineMap.lineMap_apply'`, `ContinuousAffineMap.neg_contLinear`, `ContinuousAffineMap.fderiv`, `ContinuousAffineMap.differentiableWithinAt`, `ContinuousAffineMap.fst_decompLinearEquiv`, `ContinuousAffineMap.ext_iff`, `Affine.Simplex.orthogonalProjection_vadd_smul_vsub_orthogonalProjection`, `ContinuousAffineMap.comp_apply`, `ContinuousAffineMap.prodMap_apply`, `ContinuousAffineMap.coe_mk`, `EuclideanGeometry.orthogonalProjection_congr`, `ContinuousAffineMap.neg_apply`, `ContinuousAffineMap.toFun_eq_coe`, `ContinuousAffineEquiv.coe_toContinuousAffineMap`, `ContinuousAffineMap.coe_sub`, `ContinuousAffineMap.differentiable`, `ContinuousAffineMap.smul_apply`, `EuclideanGeometry.dist_orthogonalProjection_eq_iff_oangle_eq`, `lintegral_fderiv_lineMap_eq_edist`, `AffineSubspace.coe_subtypeA`, `signedDist_right_congr`, `Affine.Simplex.sign_signedInfDist_lineMap_incenter_touchpoint`, `ContinuousAffineMap.fst_decompEquiv`, `ContinuousAffineMap.coe_to_continuousMap`, `HasFTaylorSeriesUpToOn.comp_continuousAffineMap`, `ContinuousAffineMap.coe_lineMap_eq`, `EuclideanGeometry.reflection_vadd_smul_vsub_orthogonalProjection`, `EuclideanGeometry.inter_eq_singleton_orthogonalProjection`, `signedDist_left_congr`, `signedDist_triangle`, `Affine.Simplex.orthogonalProjectionSpan_eq_point`, `signedDist_linear_apply_apply`, `ContinuousAffineMap.decomp`, `ContinuousAffineMap.zero_apply`, `EuclideanGeometry.orthogonalProjection_map`, `EuclideanGeometry.angle_orthogonalProjection_self`, `ContinuousLinearMap.toContinuousAffineMap_map_zero`, `EuclideanGeometry.orthogonalProjection_apply_mem`, `ContinuousAffineMap.smul_contLinear`, `EuclideanGeometry.dist_orthogonalProjection_eq_of_oangle_eq`, `ContinuousAffineMap.norm_def`, `signedDist_le_dist`, `EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq`, `ContinuousAffineMap.decompEquiv_symm_contLinear`, `signedDist_apply_apply`, `ContinuousAffineMap.decompLinearEquiv_symm_contLinear`, `ContinuousAffineMap.vadd_toAffineMap`, `EuclideanGeometry.dist_orthogonalProjection_eq_of_two_zsmul_oangle_eq`, `EuclideanGeometry.orthogonalProjection_apply'`, `Affine.Simplex.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq`, `ContinuousAffineMap.decompLinearIsometryEquiv_symm_apply`, `EuclideanGeometry.orthogonalProjection_orthogonalProjection_of_le`, `EuclideanGeometry.Sphere.isTangent_iff_isTangentAt_orthogonalProjection`, `Affine.Simplex.ExcenterExists.sign_signedInfDist_touchpoint`, `ContinuousAffineMap.coe_add`, `signedDist_eq_zero_of_orthogonal`, `ContinuousAffineMap.coe_toAffineMap`, `AffineSubspace.signedInfDist_eq_signedDist_of_mem`, `Affine.Simplex.signedInfDist_apply_self`, `ContinuousAffineMap.coe_injective`, `ContinuousAffineMap.norm_eq`, `signedDist_zero`, `AffineSubspace.signedInfDist_eq_signedDist_orthogonalProjection`, `Affine.Simplex.orthogonalProjectionSpan_congr`, `ContinuousAffineMap.fst_decompAffineEquiv`, `signedDist_triangle_left`, `ContinuousAffineMap.norm_contLinear_le`, `ContinuousAffineMap.coe_comp`, `EuclideanGeometry.Sphere.orthogonalProjection_orthRadius_center`, `ContinuousAffineMap.hasStrictFDerivAt`, `EuclideanGeometry.orthogonalProjection_subtype`, `EuclideanGeometry.two_zsmul_oangle_self_orthogonalProjection`, `Affine.Simplex.ExcenterExists.sign_signedInfDist_lineMap_excenter_touchpoint`, `ContinuousAffineMap.sub_contLinear`, `ContinuousAffineMap.decompLinearIsometryEquiv_symm_contLinear`, `ContinuousAffineMap.contDiff`, `EuclideanGeometry.orthogonalProjection_vadd_eq_self`, `ContinuousAffineMap.toContinuousMap_coe`, `ContinuousAffineMap.decompEquiv_symm_apply`, `signedDist_smul_of_pos`, `EuclideanGeometry.oangle_orthogonalProjection_self`, `ContinuousAffineMap.apply_lineMap'`, `signedDist_lineMap_lineMap`, `EuclideanGeometry.dist_orthogonalProjection_eq_dist_iff_eq_of_mem`, `AffineSubspace.abs_signedInfDist_eq_dist_of_mem_affineSpan_insert`, `ContinuousAffineMap.linear_decompAffineEquiv`, `signedDist_vadd_left_swap`, `Affine.Simplex.orthogonalProjection_circumcenter`, `Affine.Simplex.exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter`, `ContinuousAffineMap.instContinuousMapClass`, `signedDist_vadd_right`, `Affine.Simplex.orthogonalProjection_eq_circumcenter_of_exists_dist_eq`, `EuclideanGeometry.oangle_eq_of_dist_orthogonalProjection_eq`, `ContinuousAffineMap.map_vadd`, `EuclideanGeometry.orthogonalProjection_affineSpan_singleton`, `signedDist_lineMap_left`, `ContinuousAffineMap.coe_const`, `EuclideanGeometry.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq`, `ContinuousAffineMap.coe_zero`, `signedDist_anticomm`, `ContinuousAffineMap.add_apply`, `ContinuousAffineMap.coe_id`, `ContinuousAffineMap.decompAffineEquiv_symm_apply`, `EuclideanGeometry.orthogonalProjection_vadd_smul_vsub_orthogonalProjection`, `signedDist_triangle_right`, `Affine.Simplex.orthogonalProjectionSpan_faceOpposite_eq_point_rev`, `ContinuousAffineMap.add_contLinear`, `EuclideanGeometry.dist_orthogonalProjection_eq_infNndist`, `abs_signedDist_eq_dist_iff_vsub_mem_span`, `signedDist_neg`, `signedDist_vsub_self_rev`, `EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangent`, `ContinuousAffineMap.coe_smul`, `signedDist_linear_apply`, `EuclideanGeometry.orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem`, `ContinuousAffineMap.congr_fun`, `signedDist_self`, `ContinuousAffineMap.hasFDerivAtFilter`, `signedDist_vsub_self`, `Affine.Simplex.exists_forall_signedInfDist_eq_iff_eq_incenter`, `signedDist_smul`, `EuclideanGeometry.dist_eq_iff_dist_orthogonalProjection_eq`, `ContinuousAffineMap.hasFDerivAt`, `ContinuousAffineMap.norm_image_zero_le`, `ContinuousAffineMap.apply_lineMap`, `EuclideanGeometry.dist_orthogonalProjection_eq_infDist`, `EuclideanGeometry.orthogonalProjection_mem`, `Affine.Simplex.orthogonalProjectionSpan_restrict`, `ContinuousAffineMap.snd_decompLinearIsometryEquiv`, `signedDist_smul_of_neg`, `EuclideanGeometry.dist_orthogonalProjection_eq_zero_iff`, `Affine.Simplex.sign_signedInfDist_touchpoint_empty`, `signedDist_vadd_right_swap`, `ContinuousAffineMap.fderivWithin`, `EuclideanGeometry.exists_dist_eq_iff_exists_dist_orthogonalProjection_eq`, `EuclideanGeometry.Sphere.IsTangentAt.eq_orthogonalProjection`, `ContinuousAffineMap.sub_apply`, `ContinuousAffineMap.vadd_contLinear`, `EuclideanGeometry.reflection_eq_iff_orthogonalProjection_eq`, `AffineIsometry.toContinuousAffineMap_injective`, `EuclideanGeometry.orthogonalProjection_orthogonalProjection`, `EuclideanGeometry.orthogonalProjection_vsub_mem_direction`, `signedDist_vadd_left`, `Affine.Simplex.orthogonalProjection_eq_circumcenter_of_dist_eq`, `ContinuousAffineMap.snd_decompEquiv`, `EuclideanGeometry.vsub_orthogonalProjection_mem_direction`, `signedDist_apply_linear_apply`, `AffineSubspace.signedInfDist_singleton`, `Affine.Simplex.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection`, `ContinuousAffineMap.decompLinearEquiv_symm_apply`, `EuclideanGeometry.Sphere.IsTangent.isTangentAt`, `ContinuousAffineMap.contLinear_map_vsub`, `EuclideanGeometry.reflection_apply'`, `surjOn_extremePoints_image`, `ContinuousAffineMap.differentiableOn`, `ContinuousAffineMap.coe_continuousMap_mk`, `EuclideanGeometry.oangle_self_orthogonalProjection`, `ContinuousAffineMap.norm_comp_le`, `signedDist_right_lineMap`, `ContinuousAffineMap.vsub_toAffineMap`, `ContinuousAffineEquiv.toContinuousAffineMap_injective`, `Affine.Simplex.abs_signedInfDist_eq_dist_of_mem_affineSpan_range`, `Affine.Simplex.ExcenterExists.signedInfDist_excenter`, `Affine.Simplex.orthogonalProjectionSpan_reindex`, `AffineSubspace.signedInfDist_def`, `ContinuousAffineMap.prod_apply`, `signedDist_lineMap_right`, `Affine.Simplex.orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle`, `ContinuousAffineMap.fst_decompLinearIsometryEquiv`, `ContinuousAffineMap.vsub_apply`, `Affine.Simplex.sign_signedInfDist_incenter`, `Affine.Simplex.ExcenterExists.sign_signedInfDist_excenter`, `ContinuousAffineMap.hasFDerivWithinAt`, `Affine.Simplex.signedInfDist_affineCombination`, `signedDist_apply`, `EuclideanGeometry.angle_self_orthogonalProjection`, `signedDist_eq_dist_iff_vsub_mem_span`, `EuclideanGeometry.orthogonalProjection_eq_self_iff`, `ContinuousAffineMap.snd_decompLinearEquiv`, `Affine.Simplex.ExcenterExists.signedInfDist_excenter_eq_mul_sum_inv`, `EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal`, `Affine.Simplex.exists_forall_signedInfDist_eq_iff_excenterExists_and_eq_excenter`, `ContinuousAffineMap.snd_decompAffineEquiv`, `EuclideanGeometry.eq_orthogonalProjection_of_eq_subspace`, `ContinuousAffineMap.vsub_contLinear`, `EuclideanGeometry.orthogonalProjection_apply`, `AffineSubspace.signedInfDist_apply_self`, `EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection`, `EuclideanGeometry.orthogonalProjection_mem_orthogonal`, `ContinuousAffineMap.decompAffineEquiv_symm_contLinear`, `ContinuousAffineMap.toConstProdContinuousLinearMap_fst`, `EuclideanGeometry.two_zsmul_oangle_orthogonalProjection_self`, `abs_signedDist_le_dist`, `AffineSubspace.signedInfDist_apply_of_mem`, `EuclideanGeometry.orthogonalProjection_sup_of_orthogonalProjection_eq`, `EuclideanGeometry.coe_orthogonalProjection_eq_iff_mem`, `ContinuousLinearMap.coe_toContinuousAffineMap`, `signedDist_apply_linear`, `ContinuousAffineMap.continuous`, `ContinuousAffineMap.zero_contLinear`, `Affine.Simplex.signedInfDist_apply_of_ne`, `AffineIsometry.coe_toContinuousAffineMap`, `signedDist_left_lineMap`, `ContinuousAffineMap.coe_neg`, `EuclideanGeometry.dist_orthogonalProjection_line_eq_iff_two_zsmul_oangle_eq`, `EuclideanGeometry.orthogonalProjection_eq_iff_mem`, `EuclideanGeometry.dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq`, `ContinuousAffineMap.differentiableAt`, `ContinuousAffineMap.coe_prod`, `ContinuousAffineMap.coe_prodMap`, `EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt`, `EuclideanGeometry.dist_set_eq_iff_dist_orthogonalProjection_eq`, `ContinuousAffineMap.instIsCentralScalar`, `signedDist_vadd_vadd`, `ContinuousAffineMap.vadd_apply`, `ContinuousAffineMap.toConstProdContinuousLinearMap_snd`, `EuclideanGeometry.orthogonalProjection_mem_subspace_eq_self`, `Affine.Triangle.dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq`, `Affine.Simplex.signedInfDist_incenter`
`«term_→ᴬ[_]_»` 📖	CompOp	—

---

← Back to Index