| Name | Category | Theorems |
|---|
ContDiffWithinAtProp 📖 | MathDef | 11 mathmath: contDiffWithinAtProp_self, smoothSheafCommRing.eval_germ, contDiffWithinAtProp_id, smoothSheafCommRing.evalHom_germ, contDiffWithinAtProp_self_source, contDiffWithinAt_localInvariantProp, contDiffWithinAt_localInvariantProp_of_le, contDiffWithinAtProp_mono_of_mem_nhdsWithin, contDiffWithinAtProp_self_target, smoothSheaf.eval_germ, smoothSheaf.contMDiff_section
|
ContMDiff 📖 | MathDef | 181 mathmath: contMDiff_prod_assoc, contMDiff_congr, Bundle.ContMDiffRiemannianMetric.contMDiff, ContMDiff.div₀, ContMDiff.comp, contMDiff_finprod, ContMDiff.of_comp_isOpenEmbedding, contMDiff_finset_prod', contMDiff_addInvariantVectorField, contMDiff_neg_sphere, ContMDiff.sub_const, SmoothBumpCovering.exists_immersion_euclidean, IsOpen.exists_msmooth_support_eq, ContMDiffMul.contMDiff_mul, ContMDiff.of_succ, ContMDiff.clm_apply, contMDiff_mul, contMDiff_mulInvariantVectorField, ContMDiff.along_snd, contMDiff_sum_map, contMDiff_equivTangentBundleProd_symm, contMDiff_finprod_cond, contMDiff_add_right, contMDiff_inclusion, ContinuousLinearMap.contMDiff, contMDiff_finset_prod, contMDiff_mul_right, contMDiff_infty, ContMDiffMonoidMorphism.contMDiff_toFun, ContMDiff.coordChange, contMDiff_pow, ContMDiffAdd.contMDiff_add, contMDiff_of_contMDiff_inl, ContMDiff.smul, Diffeomorph.contMDiff_comp_diffeomorph_iff, ContMDiff.inr, Diffeomorph.contMDiff_toFun, contMDiff_mul_left, ContMDiff.sum_section_of_locallyFinite, ContMDiff.contMDiff_tangentMap, ContMDiff.piecewise_Iic, UpperHalfPlane.contMDiff_coe, contMDiff_coe_sphere, IsOpen.exists_contMDiff_support_eq_aux, ContMDiff.inv, contMDiff_isOpenEmbedding, contMDiff_model, ContMDiff.mul, UpperHalfPlane.contMDiff_inv_denom, ContMDiff.sumMap, contMDiff_of_discreteTopology, ContMDiff.nsmul, BumpCovering.contMDiff_toPartitionOfUnity, contMDiff_zero_iff, ContMDiff.inl, ContMDiff.congr, contMDiff_vectorSpace_iff_contDiff, ContDiff.comp_contMDiff, IsLocalDiffeomorph.contMDiff, ContMDiff.div, IsContMDiffRiemannianBundle.exists_contMDiff, contMDiff_snd, contMDiff_subtype_coe_Icc, contMDiff_const, contMDiff_iff_contDiff, contMDiff_iff_target, ContMDiff.fst, UpperHalfPlane.contMDiff_num, ContMDiffMap.contMDiff, ContMDiff.swap, ContMDiff.pow, contMDiff_of_tsupport, IsOpen.exists_contMDiff_support_eq, contMDiff_finsum_cond, contMDiff_smul, contMDiff_of_contMDiffOn_union_of_isOpen, contMDiff_neg, contMDiff_of_mulTSupport, ContMDiffOn.comp_contMDiff, ContMDiff.add, exists_msmooth_support_eq_eq_one_iff, LieGroup.contMDiff_inv, exists_msmooth_zero_iff_one_iff_of_isClosed, ContMDiff.extend_zero, ContMDiffRing.contMDiff_mul, contMDiff_prod_iff, ContDiff.contMDiff, contMDiff_of_contMDiff_inr, ContMDiff.finsum_section_of_locallyFinite, Manifold.riemannianEDist_def, contMDiff_one, ContMDiff.sub, UpperHalfPlane.contMDiff_denom_zpow, ContMDiff.clm_bundle_apply, ContMDiff.inv₀, ContMDiff.clm_bundle_apply₂, IsOpen.exists_msmooth_support_eq_aux, exists_contMDiff_zero_iff_one_iff_of_isClosed, SmoothBumpFunction.contMDiff_smul, Bundle.contMDiff_proj, Diffeomorph.contMDiff_invFun, LieAddGroup.contMDiff_neg, contMDiff_inv, ContinuousLinearEquiv.contMDiff_transContinuousLinearEquiv_right, contMDiff_iff, ContMDiff.sumElim, ContMDiff.neg_section, ContMDiffAddMonoidMorphism.contMDiff_toFun, contMDiff_finsum, Bundle.Trivialization.contMDiff_iff, contMDiff_of_contMDiffOn_iUnion_of_isOpen, Bundle.contMDiff_zeroSection, ContDiff.mlieBracket_vectorField, contMDiff_prod_module_iff, contMDiffOn_univ, ContMDiff.clm_postcomp, ContMDiff.inner_bundle, contMDiff_id, ContMDiff.clm_prodMap, exists_contMDiff_support_eq_eq_one_iff, ContMDiffSection.contMDiff, contMDiff_equivTangentBundleProd, ContMDiff.piecewise, SmoothPartitionOfUnity.contMDiff_finsum_smul, contMDiff_zero, contMDiff_finset_sum, ContMDiff.iterate, ContMDiff.of_le, contMDiffOn_comp_projIcc_iff, SmoothBumpFunction.contMDiff, smoothSheaf.contMDiff_section, contMDiff_add, contMDiff_of_locally_contMDiffOn, exists_embedding_euclidean_of_compact, ContinuousLinearEquiv.contMDiff_transContinuousLinearEquiv_left, ContMDiff.sub_section, Units.contMDiff_val, contMDiff_tangentBundleModelSpaceHomeomorph, ContMDiffOn.smul_section_of_tsupport, ContMDiff.div_const, contMDiff_pi_space, contMDiff_nsmul, Diffeomorph.contMDiff_diffeomorph_comp_iff, ContMDiff.extend_one, ContMDiff.clm_comp, contMDiff_tangentBundleModelSpaceHomeomorph_symm, ContMDiff.snd, contMDiff_of_subsingleton, ContMDiff.clm_precomp, ContMDiff.add_section, Diffeomorph.contMDiff, ContMDiff.codRestrict_sphere, ContMDiff.curry_right, SmoothPartitionOfUnity.contMDiff_smul, ContMDiffMap.coeFn_mk, ContMDiff.prodMk_space, ContMDiff.prod, ContMDiff.const_smul_section, UpperHalfPlane.contMDiff_smul, UpperHalfPlane.contMDiff_denom, ContMDiffSection.contMDiff_toFun, SmoothPartitionOfUnity.IsSubordinate.contMDiff_finsum_smul, ContMDiff.neg, contMDiff_finset_sum', contMDiff_fst, Manifold.exists_lt_locally_constant_of_riemannianEDist_lt, ContMDiff.sum_section, ContMDiff.prodMap, contMDiff_snd_tangentBundle_modelSpace, ContMDiff.sum, contMDiff_subtype_val, ContMDiff.cle_arrowCongr, ContMDiff.mpullback_vectorField, ContMDiff.coordChangeL, SmoothPartitionOfUnity.contMDiff_sum, contMDiff_add_left, ContMDiff.smul_section, contMDiff_circleExp, ContMDiff.along_fst, ContMDiff.curry_left, ContMDiff.prodMk
|
ContMDiffAt 📖 | MathDef | 138 mathmath: ContMDiffAt.coordChangeL, contMDiffAt_add_right, ContMDiffAt.inv, ContMDiffAt.comp₂, contMDiffAt_extend, ContinuousLinearEquiv.contMDiffAt_transContinuousLinearEquiv_right, contMDiffAt_iff_of_mem_source, contMDiffAt_finset_prod, ContDiffAt.contMDiffAt, contMDiffAt_iff_source, SmoothPartitionOfUnity.contMDiffAt_finsum, contMDiffAt_iff_le_ne_infty, ContMDiffAt.finsum_section_of_locallyFinite, IsLocalFrameOn.contMDiffAt_of_coeff, ContMDiffAt.div_const, ContMDiffAt.clm_postcomp, ContMDiffAt.add_section, ContMDiffAt.mfderiv_apply, ContMDiffAt.div₀, Bundle.contMDiffAt_zeroSection, contMDiffAt_mulInvariantVectorField, contMDiffAt_add_left, contMDiffAt_const, ContMDiffAt.smul, ContinuousLinearEquiv.contMDiffAt_transContinuousLinearEquiv_left, ContMDiffAt.prodMap, contMDiffAt_iff_source_of_mem_source, ContMDiffAt.curry_left, ContMDiffAt.const_smul_section, ContMDiffWithinAt.contMDiffAt, ContMDiffAt.mfderiv_const, ContMDiffAt.clm_apply_of_inCoordinates, contMDiffAt_iff_contMDiffOn_nhds, ContMDiffAt.comp₂_of_eq, SmoothBumpFunction.contMDiffAt, contMDiffAt_finprod, ContMDiffAt.clm_bundle_apply, contMDiffAt_prod_iff, contMDiffAt_coordChangeL, ContMDiffAt.of_succ, ContMDiffAt.prodMk_space, ContMDiffInv₀.contMDiffAt_inv₀, ContMDiffAt.snd, ContMDiffAt.prod, Diffeomorph.contMDiffAt_diffeomorph_comp_iff, contMDiffAt_iff, ContMDiffAt.neg, ContDiffAt.comp_contMDiffAt, ContMDiffAt.pow, ContMDiffAt.div, contMDiffAt_of_notMem, ContMDiffAt.of_le, ContMDiffAt.along_fst, ContMDiffAt.along_snd, contMDiffAt_iff_contMDiffAt_nhds, IsLocalFrameOn.contMDiffAt, contMDiffAt_hom_bundle, ContMDiffAt.inv₀, ContMDiffAt.mlieBracket_vectorField, ContMDiffAt.clm_precomp, contMDiffAt_id, contMDiffAt_localFrame_coeff, contMDiffAt_finset_sum, contMDiffAt_one, Bundle.contMDiffAt_totalSpace, ContMDiffAt.comp_of_eq, ContMDiffAt.congr_of_eventuallyEq, Diffeomorph.contMDiffAt_comp_diffeomorph_iff, contMDiffWithinAt_comp_projIcc_iff, contMDiffAt_iff_nat, Filter.EventuallyEq.contMDiffAt_iff, FiberBundle.contMDiffAt_extend', ContMDiffAt.nsmul, contMDiffAt_iff_target_of_mem_source, IsLocalDiffeomorphAt.localInverse_contMDiffAt, contMDiffAt_vectorSpace_iff_contDiffAt, ContMDiffAt.clm_prodMap, ContMDiffAt.curry_right, contMDiffAt_extChartAt, ContMDiffOn.contMDiffAt, contMDiffAt_symm_of_mem_maximalAtlas, ContMDiffAt.sum, contMDiffAt_localFrame_of_mem, Bundle.Trivialization.contMDiffAt_section_iff, Diffeomorph.contMDiffAt, ContMDiffAt.sub_section, ContMDiffAt.inner_bundle, contMDiffAt_subtype_iff, Bundle.Trivialization.contMDiffAt_iff, Bundle.contMDiffAt_section, ContMDiffAt.fst, ContMDiffAt.clm_bundle_apply₂, contMDiffAt_iff_localFrame_coeff, contMDiffAt_prod_module_iff, contMDiffWithinAt_univ, ContMDiffAt.prodMap', UpperHalfPlane.contMDiffAt_ofComplex, ContMDiffAt.sum_section_of_locallyFinite, ContMDiffAt.mfderiv, UpperHalfPlane.contMDiffAt_iff, contMDiffAt_of_mem_maximalAtlas, ContMDiffAt.prodMk, Bundle.contMDiffAt_proj, contMDiffAt_addInvariantVectorField, ContMDiffAt.sub, ContMDiffAt.mpullback_vectorField_preimage, contMDiffAt_extChartAt', ContMDiffAt.clm_apply, contMDiffAt_infty, ContMDiff.contMDiffAt, contMDiffAt_mul_right, contMDiffAt_of_subsingleton, ContMDiffAt.coordChange, contMDiffAt_mul_left, contMDiffAt_finsum, contMDiffAt_fst, contMDiffAt_finset_prod', contMDiffAt_inv₀, ContMDiffAt.sum_section, ContMDiffAt.sub_const, ContMDiffAt.comp, contMDiffAt_pi_space, contMDiffAt_iff_target, ContMDiffAt.smul_section, contMDiffAt_finset_sum', ContMDiffAt.clm_comp, IsLocalDiffeomorphAt.contMDiffAt, ContMDiffAt.neg_section, IsLocalFrameOn.contMDiffAt_of_coeff_aux, ContMDiffAt.cle_arrowCongr, ContinuousLinearMap.contMDiffAt, contMDiffAt_iff_contDiffAt, ContMDiffAt.add, contMDiffAt_snd, ContDiff.comp_contMDiffAt, ContMDiffAt.mul, contMDiffAt_zero, contMDiffAt_of_notMem_mulTSupport
|
ContMDiffOn 📖 | MathDef | 151 mathmath: contMDiffOn_of_subsingleton, Bundle.contMDiffOn_zeroSection, contMDiffOn_finsum, Diffeomorph.contMDiffOn_comp_diffeomorph_iff, ContMDiffOn.prodMk, ContMDiffOn.mlieBracketWithin_vectorField, PartialDiffeomorph.contMDiffOn, ContMDiffOn.of_succ, contMDiffOn_chart, Bundle.Trivialization.contMDiffOn_section_baseSet_iff, ContMDiffOn.clm_postcomp, Bundle.Trivialization.contMDiffOn, contMDiffOn_of_locally_contMDiffOn, contMDiffOn_localFrame_coeff, OpenPartialHomeomorph.contMDiffOn_writtenInExtend_iff, VectorBundleCore.contMDiffOn_coordChange, contMDiffOn_chart_symm, contMDiffOn_baseSet_iff_localFrame_coeff, PartialDiffeomorph.contMDiffOn_toFun, contMDiffOn_isOpenEmbedding_symm, contMDiffOn_finset_prod, contMDiffOn_inv₀, ContMDiffOn.of_le, contMDiffOn_iff_contDiffOn, contMDiffOn_finset_sum, ContDiffOn.contMDiffOn, ContMDiffFiberwiseLinear.locality_aux₂, ContMDiffOn.finsum_section_of_locallyFinite, ContMDiffOn.clm_precomp, ContMDiffOn.coordChangeL, IsLocalDiffeomorphAt.localInverse_contMDiffOn, contMDiffOn_pi_space, ContMDiffOn.mul, ContMDiffOn.mpullbackWithin_vectorField_inter, contMDiffAt_iff_contMDiffOn_nhds, FiberBundle.exists_contMDiffOn_extend, ContMDiffOn.cle_arrowCongr, Bundle.Trivialization.contMDiffOn_localFrame_baseSet, contMDiffOn_zero, ContMDiffOn.along_snd, ContMDiffOn.curry_right, contMDiff_iff_target, ContMDiffOn.clm_comp, contMDiffOn_extChartAt, ContMDiff.contMDiffOn, contMDiffOn_baseSet_localFrame_coeff, contMDiffOn_finset_prod', ContMDiffOn.div, contMDiffOn_iff_of_mem_maximalAtlas', contMDiffOn_continuousLinearMapCoordChange, contMDiffOn_extChartAt_symm, IsLocalFrameOn.contMDiffOn, IsLocalDiffeomorphAt.contmdiffOn_localInverse, IsLocalDiffeomorphOn.contMDiffOn, contMDiffOn_iff_of_subset_source', ContMDiffOn.prodMk_space, isLocalStructomorphOn_contDiffGroupoid_iff, contMDiffWithinAt_iff_contMDiffOn_nhds, contMDiffOn_iUnion_iff_of_isOpen, contMDiffOn_of_mem_contDiffGroupoid, contMDiffOn_symm_coordChangeL, ContMDiffOn.prodMap, ContMDiffOn.add_section, ContMDiffOn.inner_bundle, ContMDiff.comp_contMDiffOn, ContMDiffOn.clm_apply, contMDiffOn_finset_sum', ContMDiffOn.curry_left, Diffeomorph.contMDiffOn_diffeomorph_comp_iff, ContMDiffOn.iterate, ContMDiffOn.sub_const, ContMDiffOn.mono, Bundle.contMDiffOn_proj, contMDiffOn_fst, contMDiffOn_prod_iff, contMDiffOn_iff, contMDiffOn_iff_source_of_mem_maximalAtlas, ContMDiffWithinAt.contMDiffOn', ContMDiffOn.comp', contMDiffOn_finprod, ContMDiffVectorBundle.contMDiffOn_coordChangeL, VectorBundleCore.IsContMDiff.contMDiffOn_coordChange, ContMDiffOn.congr, contMDiffOn_univ, contMDiffOn_iff_of_mem_maximalAtlas, ContMDiffOn.const_smul_section, contMDiffOn_iff_of_subset_source, Bundle.Trivialization.contMDiffOn_symm, ContMDiffOn.nsmul, ContMDiffOn.sum_section_of_locallyFinite, contMDiffOn_of_mem_maximalAtlas, ContMDiffCovariantDerivativeOn.contMDiff, contMDiffOn_comp_projIcc_iff, ContMDiffOn.contMDiffOn_tangentMapWithin, contMDiffOn_const, ContMDiffOn.sub, ContMDiffFiberwiseLinear.locality_aux₁, PartialDiffeomorph.contMDiffOn_invFun, ContMDiffOn.mpullback_vectorField_preimage, IsLocalFrameOn.contMDiffOn_of_coeff, ContMDiffOn.iUnion_of_isOpen, ContMDiffOn.div_const, contMDiffOn_extend_symm, VectorPrebundle.contMDiffOn_contMDiffCoordChange, ContMDiffOn.along_fst, ContMDiffOn.coordChange, ContMDiffOn.congr_mono, isLocalStructomorphOn_contDiffGroupoid_iff_aux, VectorPrebundle.IsContMDiff.exists_contMDiffCoordChange, ContinuousLinearMap.contMDiffOn, contMDiffOn_coordChangeL, contMDiffOn_model_symm, ContinuousLinearEquiv.contMDiffOn_transContinuousLinearEquiv_left, ContMDiffOn.inv, ContMDiffOn.sub_section, ContMDiffOn.clm_prodMap, ContMDiffOn.sum_section, ContMDiffOn.neg_section, ContMDiffWithinAt.contMDiffOn, Bundle.Trivialization.contMDiffOn_iff, ContMDiffOn.smul, contMDiffOn_extend, contMDiffOn_one, contMDiffOn_empty, contMDiffOn_union_iff_of_isOpen, contMDiffOn_iff_target, contMDiffOn_symm_of_mem_maximalAtlas, contMDiffOn_vectorSpace_iff_contDiffOn, ContMDiffOn.neg, ContMDiffOn.clm_bundle_apply, Manifold.exists_lt_of_riemannianEDist_lt, Bundle.Trivialization.contMDiffOn_section_iff, contMDiffOn_zero_iff, ContMDiffOn.union_of_isOpen, contMDiffOn_snd, ContMDiffOn.add, contMDiffOn_prod_module_iff, contMDiffOn_congr, Bundle.Trivialization.contMDiffOn_symm_trans, mem_contMDiffFiberwiseLinear_iff, contMDiffOn_id, ContMDiffOn.div₀, contMDiffOn_infty, ContMDiffOn.clm_bundle_apply₂, ContinuousLinearEquiv.contMDiffOn_transContinuousLinearEquiv_right, ContMDiffOn.comp, contMDiffOn_projIcc, ContMDiffOn.pow, ContMDiffOn.inv₀, ContMDiffOn.smul_section, contMDiffOn_iff_localFrame_coeff
|
ContMDiffWithinAt 📖 | MathDef | 155 mathmath: ContMDiffWithinAt.sub, contMDiffWithinAt_insert_self, Diffeomorph.contMDiffWithinAt, contMDiffWithinAt_iff_target, contMDiffWithinAt_congr_set', ContMDiffWithinAt.comp_of_eq, ContDiffWithinAt.contMDiffWithinAt, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt, ContMDiffWithinAt.mono, ContMDiffWithinAt.mlieBracketWithin_vectorField, contMDiffWithinAt_congr_of_mem, contMDiffWithinAt_iff_contMDiffWithinAt_nhdsWithin, contMDiffAt_iff_source, ContMDiffAt.contMDiffWithinAt, contMDiffWithinAt_inter', ContMDiffWithinAt.sub_section, ContMDiffWithinAt.mfderivWithin_const, Bundle.contMDiffWithinAt_zeroSection, contMDiffWithinAt_iff_image, contMDiffWithinAt_snd, contMDiffWithinAt_prod_iff, ContMDiffWithinAt.clm_postcomp, ContMDiffWithinAt.nsmul, ContMDiffWithinAt.coordChange, ContMDiffWithinAt.snd, ContMDiffWithinAt.add_section, contMDiffWithinAt_congr_set, contMDiffWithinAt_prod_module_iff, ContMDiffWithinAt.pow, ContMDiffWithinAt.sum_section, ContDiffAt.comp_contMDiffWithinAt, contMDiffWithinAt_finset_prod, contMDiffWithinAt_pi_space, ContMDiffWithinAt.congr', contMDiffAt_iff_source_of_mem_source, ContMDiffWithinAt.neg_section, ContMDiffWithinAt.mpullbackWithin_vectorField_inter, ContMDiffWithinAt.inv, ContMDiffWithinAt.fst, ContMDiffWithinAt.change_section_trivialization, ContMDiffWithinAt.prodMk_space, contMDiffWithinAt_finset_sum, ContMDiffAt.comp_contMDiffWithinAt_of_eq, contMDiffWithinAt_const, ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin_of_eq, contMDiffWithinAt_zero, ContMDiffWithinAt.mpullback_vectorField_preimage, contMDiffWithinAt_iff_of_mem_source', ContMDiffWithinAt.comp', ContDiff.comp_contMDiffWithinAt, ContMDiffWithinAt.comp₂, ContMDiffWithinAt.mpullback_vectorField_preimage_of_eq, ContMDiffWithinAt.congr_of_mem, contMDiffWithinAt_finprod, ContMDiffWithinAt.prod, contMDiffWithinAt_extChartAt_symm_range_self, contMDiffWithinAt_iff_target_of_mem_source, ContMDiffWithinAt.finsum_section_of_locallyFinite, Bundle.contMDiffWithinAt_totalSpace, contMDiffWithinAt_iff_source_of_mem_maximalAtlas, ContMDiffWithinAt.smul, ContMDiffWithinAt.curry_right, Bundle.Trivialization.contMDiffWithinAt_iff, ContMDiffWithinAt.add, ContMDiffWithinAt.mpullbackWithin_vectorField', contMDiffWithinAt_one, contMDiffWithinAt_iff_contMDiffOn_nhds, contMDiffWithinAt_iff_le_ne_infty, ContMDiffWithinAt.clm_bundle_apply₂, contMDiffWithinAt_iff, ContMDiffWithinAt.mono_of_mem_nhdsWithin, contMDiffWithinAt_of_subsingleton, ContMDiffWithinAt.congr_of_eventuallyEq_of_mem, Bundle.contMDiffWithinAt_proj, contMDiffWithinAt_id, ContMDiffWithinAt.clm_bundle_apply, ContinuousLinearEquiv.contMDiffWithinAt_transContinuousLinearEquiv_right, contMDiffWithinAt_comp_projIcc_iff, ContMDiffWithinAt.div, ContMDiffWithinAt.along_fst, ContMDiffWithinAt.mfderivWithin, ContMDiffWithinAt.of_insert, contMDiffWithinAt_fst, ContMDiffWithinAt.prodMk, contMDiffWithinAt_iff', ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem_of_eq, Diffeomorph.contMDiffWithinAt_comp_diffeomorph_iff, contMDiffWithinAt_extChartAt_symm_target_self, contMDiffWithinAt_inter, ContMDiffWithinAt.inv₀, ContMDiffWithinAt.comp₂_of_eq, contMDiffWithinAt_iff_contDiffWithinAt, contMDiffWithinAt_finset_sum', ContMDiffWithinAt.mfderivWithin_apply, ContMDiffWithinAt.congr, VectorField.contMDiffWithinAt_mpullbackWithin_extChartAt_symm, ContMDiffWithinAt.sum_section_of_locallyFinite, ContinuousLinearEquiv.contMDiffWithinAt_transContinuousLinearEquiv_left, contMDiffWithinAt_extChartAt_symm_target, ContMDiffWithinAt.of_le, ContMDiffWithinAt.of_succ, ContMDiffWithinAt.clm_apply_of_inCoordinates, contMDiffWithinAt_iff_source, Bundle.Trivialization.contMDiffWithinAt_section, ContMDiffWithinAt.congr_set, contMDiffWithinAt_iff_source_of_mem_source, ContMDiffWithinAt.mpullbackWithin_vectorField_inter_of_eq, ContMDiffWithinAt.along_snd, contMDiffWithinAt_iff_of_mem_maximalAtlas, contMDiffWithinAt_univ, ContMDiffWithinAt.sub_const, ContMDiffWithinAt.clm_apply, contMDiffWithinAt_infty, ContMDiffWithinAt.sum, contMDiffWithinAt_extChartAt_symm_range, ContMDiffWithinAt.coordChangeL, ContMDiffWithinAt.div_const, ContMDiffWithinAt.const_smul_section, ContMDiffWithinAt.prodMap', Diffeomorph.contMDiffWithinAt_diffeomorph_comp_iff, ContinuousLinearMap.contMDiffWithinAt, ContMDiffWithinAt.mpullbackWithin_vectorField, ContMDiffWithinAt.congr_of_eventuallyEq, ContMDiffWithinAt.clm_prodMap, ContMDiffWithinAt.mul, contMDiffWithinAt_finsum, OpenPartialHomeomorph.contMDiffWithinAt_writtenInExtend_iff, ContMDiffWithinAt.smul_section, Bundle.contMDiffWithinAt_section, ContMDiffWithinAt.div₀, ContMDiffWithinAt.clm_precomp, contMDiffWithinAt_of_notMem_mulTSupport, ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq, ContMDiffWithinAt.neg, ContMDiffWithinAt.clm_comp, ContMDiffAt.comp_contMDiffWithinAt, ContMDiffWithinAt.prodMap, ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem, VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm, Bundle.Trivialization.contMDiffWithinAt_snd_comp_iff₂, ContMDiffWithinAt.cle_arrowCongr, contMDiffWithinAt_of_notMem, contMDiffWithinAt_iff_nat, contMDiffWithinAt_congr, ContMDiffWithinAt.inner_bundle, contMDiffWithinAt_finset_prod', Filter.EventuallyEq.contMDiffWithinAt_iff, ContMDiffWithinAt.curry_left, ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq', contMDiffWithinAt_hom_bundle, ContDiffWithinAt.comp_contMDiffWithinAt, contMDiffWithinAt_iff_of_mem_source, ContMDiffWithinAt.insert, ContMDiffWithinAt.comp, ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin
|