| Name | Category | Theorems |
|---|
DifferentiableWithinAtProp 📖 | MathDef | 4 mathmath: differentiableWithinAtProp_self_source, DifferentiableWithinAtProp_self, differentiableWithinAt_localInvariantProp, differentiableWithinAtProp_self_target
|
HasMFDerivAt 📖 | MathDef | 32 mathmath: HasMFDerivAt.mul, HasMFDerivAt.add, HasMFDerivAt.congr_mfderiv, hasMFDerivAt_extChartAt, hasMFDerivAt_sumSwap, hasMFDerivAt_fst, HasMFDerivAt.smul, HasMFDerivAt.neg, ModelWithCorners.hasMFDerivAt, hasMFDerivAt_inr, MDifferentiableAt.hasMFDerivAt, hasMFDerivAt_neg, ContinuousLinearEquiv.hasMFDerivAt, HasFDerivAt.hasMFDerivAt, HasMFDerivAt.prodMap, hasMFDerivAt_id, hasMFDerivAt_inl, IsMIntegralCurveAt.hasMFDerivAt, hasMFDerivAt_const, ContinuousLinearMap.hasMFDerivAt, hasMFDerivWithinAt_univ, HasMFDerivAt.sub, HasMFDerivAt.prod, HasMFDerivAt.congr_of_eventuallyEq, hasMFDerivAt_iff_hasFDerivAt, HasMFDerivAt.prodMk, hasMFDerivAt_snd, HasMFDerivAt.sum, HasMFDerivAt.comp, HasMFDerivAt.mul', HasMFDerivWithinAt.hasMFDerivAt, HasMFDerivAt.const_smul
|
HasMFDerivWithinAt 📖 | MathDef | 42 mathmath: MDifferentiableWithinAt.hasMFDerivWithinAt, HasMFDerivWithinAt.insert, hasMFDerivWithinAt_insert, HasMFDerivWithinAt.prodMk, HasMFDerivWithinAt.insert', mdifferentiableWithinAt_iff_exists_hasMFDerivWithinAt, HasMFDerivWithinAt.prodMap, hasMFDerivWithinAt_diff_singleton, HasMFDerivWithinAt.neg, ContinuousLinearEquiv.hasMFDerivWithinAt, hasMFDerivWithinAt_extChartAt, hasMFDerivWithinAt_inr, hasMFDerivWithinAt_id, hasMFDerivWithinAt_fst, hasMFDerivWithinAt_inter', HasMFDerivWithinAt.sum, ModelWithCorners.hasMFDerivWithinAt, HasMFDerivWithinAt.mul', HasMFDerivWithinAt.congr_of_eventuallyEq, HasFDerivWithinAt.hasMFDerivWithinAt, HasMFDerivWithinAt.mono_of_mem_nhdsWithin, hasMFDerivWithinAt_const, ModelWithCorners.hasMFDerivWithinAt_symm, hasMFDerivWithinAt_univ, HasMFDerivAt.hasMFDerivWithinAt, HasMFDerivWithinAt.add, HasMFDerivWithinAt.congr_mfderiv, HasMFDerivAt.comp_hasMFDerivWithinAt, hasMFDerivWithinAt_snd, hasMFDerivWithinAt_congr_set, hasMFDerivWithinAt_inter, HasMFDerivWithinAt.mul, HasMFDerivWithinAt.mono, HasMFDerivWithinAt.union, ContinuousLinearMap.hasMFDerivWithinAt, HasMFDerivWithinAt.of_insert, HasMFDerivWithinAt.comp, HasMFDerivWithinAt.prod, hasMFDerivWithinAt_inl, HasMFDerivWithinAt.congr_mono, hasMFDerivWithinAt_iff_hasFDerivWithinAt, hasMFDerivWithinAt_congr_set'
|
MDifferentiableAt 📖 | MathDef | 101 mathmath: Bundle.mdifferentiableAt_proj, mdifferentiableAt_sub_section, MDifferentiableAt.prod, MDifferentiableAt.clm_bundle_apply, MDifferentiableAt.cle_arrowCongr, MDifferentiable.mdifferentiableAt, mdifferentiableAt_iff_localFrame_coeff, MDifferentiableAt.sum, mdifferentiableAt_add_section, ContMDiffAt.mdifferentiableAt, Differentiable.comp_mdifferentiableAt, mdifferentiableWithinAt_univ, MDifferentiableOn.mdifferentiableAt, IsLocalDiffeomorphAt.localInverse_mdifferentiableAt, OpenPartialHomeomorph.MDifferentiable.mdifferentiableAt_symm, mdifferentiableAt_iff, MDifferentiableAt.snd, MDifferentiableAt.comp_of_eq, MDifferentiableAt.mul, mdifferentiableAt_of_mfderiv_injective, MDifferentiableAt.clm_prodMap, MDifferentiableAt.pow, MDifferentiableAt.clm_postcomp, mdifferentiableAt_addInvariantVectorField, MDifferentiableAt.add, MDifferentiableAt.mpullback_vectorField, mdifferentiableAt_mul_right, MDifferentiableAt.sum_section, mdifferentiableAt_fst, Bundle.Trivialization.mdifferentiableAt_section_iff, MDifferentiableAt.prodMap', mdifferentiableAt_totalSpace, MDifferentiableAt.prodMk, mdifferentiableAt_hom_bundle, IsLocalFrameOn.mdifferentiableAt_of_coeff_aux, mdifferentiableAt_snd, MDifferentiableAt.finsum_section_of_locallyFinite, MDifferentiableAt.const_smul, mdifferentiableAt_neg_section, MDifferentiableAt.clm_bundle_apply₂, mdifferentiableAt_add_right, MDifferentiableAt.congr_of_eventuallyEq, MDifferentiableAt.smul_section, mdifferentiableAt_prod_module_iff, FiberBundle.mdifferentiableAt_extend, MDifferentiableAt.sub, MDifferentiableAt.clm_comp, ModelWithCorners.mdifferentiableAt, mdifferentiableAt_mul_left, mdifferentiableAt_add_left, MDifferentiableAt.coordChange, MDifferentiableAt.clm_apply_of_inCoordinates, MDifferentiableAt.prodMk_space, mdifferentiableAt_iff_target_of_mem_source, HasMFDerivAt.mdifferentiableAt, MDifferentiableAt.smul, mdifferentiableAt_prod_iff, MDifferentiableAt.clm_precomp, mdifferentiableAt_of_isInvertible_mfderiv, MDifferentiableAt.neg, MDifferentiableAt.sum_section_of_locallyFinite, IsLocalDiffeomorphAt.mdifferentiableAt, mdifferentiableAt_neg, MDifferentiableWithinAt.mdifferentiableAt, mdifferentiableWithinAt_comp_projIcc_iff, mdifferentiableAt_section, mdifferentiableAt_const, MDifferentiableAt.coordChangeL, mdifferentiableAt_atlas_symm, PartialDiffeomorph.mdifferentiableAt, mdifferentiableAt_id, mdifferentiableAt_mulInvariantVectorField, mdifferentiableAt_iff_source_of_mem_source, mdifferentiableAt_iff_of_mem_source, ContMDiffMap.mdifferentiableAt, mdifferentiableAt_iff_differentiableAt, OpenPartialHomeomorph.MDifferentiable.mdifferentiableAt, mdifferentiableAt_coordChangeL, MDifferentiableAt.comp, MDifferentiableAt.smul_const_section, mdifferentiableAt_iff_target, MDifferentiableAt.inner_bundle, ContMDiffSection.mdifferentiableAt, UpperHalfPlane.mdifferentiableAt_iff, Bundle.Trivialization.mdifferentiableAt_snd_comp_iff₂, IsLocalFrameOn.mdifferentiableAt_of_coeff, DifferentiableAt.mdifferentiableAt, mdifferentiableAt_localFrame_coeff, ContMDiff.mdifferentiableAt, MDifferentiableAt.fst, mdifferentiableAt_atlas, Bundle.mdifferentiableAt_zeroSection, ContinuousLinearEquiv.mdifferentiableAt, MDifferentiableAt.prodMap, mdifferentiableAt_extChartAt, Filter.EventuallyEq.mdifferentiableAt_iff, UpperHalfPlane.mdifferentiableAt_ofComplex, Bundle.Trivialization.mdifferentiableAt_totalSpace_iff, ContinuousLinearMap.mdifferentiableAt, DifferentiableAt.comp_mdifferentiableAt, MDifferentiableAt.clm_apply
|
MDifferentiableOn 📖 | MathDef | 83 mathmath: mdifferentiableOn_of_locally_mdifferentiableOn, MDifferentiableOn.clm_postcomp, MDifferentiableOn.finsum_section_of_locallyFinite, mdifferentiableOn_iff, mdifferentiable_iff_target, MDifferentiableOn.prodMk_space, MDifferentiableOn.smul_const_section, mdifferentiableOn_empty, mdifferentiableOn_extChartAt, mdifferentiableOn_symm_coordChangeL, ModelWithCorners.mdifferentiableOn_symm, mdifferentiableOn_snd, MDifferentiableOn.congr, mdifferentiableOn_id, MDifferentiable.comp_mdifferentiableOn, Diffeomorph.mdifferentiableOn, MDifferentiableOn.mono, MDifferentiableOn.smul, mdifferentiableOn_iff_target, MDifferentiableOn.prodMk, mdifferentiableOn_fst, mdifferentiableOn_prod_module_iff, MDifferentiableOn.sum_section_of_locallyFinite, mdifferentiableOn_localFrame_coeff, mdifferentiableOn_iUnion_iff_of_isOpen, Bundle.Trivialization.mdifferentiableOn_section_baseSet_iff, MDifferentiableOn.coordChangeL, MDifferentiableOn.clm_prodMap, MDifferentiableOn.comp, IsLocalFrameOn.mdifferentiableOn_of_coeff, MDifferentiableOn.congr_mono, mdifferentiableOn_extChartAt_symm, MDifferentiableOn.prodMap, MDifferentiableOn.add, MDifferentiableOn.prod, DifferentiableOn.mdifferentiableOn, ContinuousLinearEquiv.mdifferentiableOn, MDifferentiableOn.clm_bundle_apply, Bundle.Trivialization.mdifferentiableOn_section_iff, mdifferentiableOn_iff_of_subset_source, Bundle.mdifferentiableOn_proj, MDifferentiableOn.sum, MDifferentiableOn.inner_bundle, mdifferentiableOn_baseSet_localFrame_coeff, MDifferentiableOn.cle_arrowCongr, MDifferentiableOn.sum_section, MDifferentiableOn.clm_apply, mdifferentiableOn_continuousLinearMapCoordChange, MDifferentiableOn.mpullback_vectorField_preimage, PartialDiffeomorph.mdifferentiableOn, mdifferentiableOn_atlas, MDifferentiableOn.clm_comp, mdifferentiableOn_iff_of_mem_maximalAtlas', mdifferentiableOn_iff_differentiableOn, mdifferentiableOn_coordChangeL, MDifferentiableOn.iUnion_of_isOpen, MDifferentiableOn.clm_precomp, MDifferentiableOn.coordChange, MDifferentiableOn.mpullbackWithin_vectorField_inter, mDifferentiableOn_sub_section, mdifferentiableOn_prod_iff, MDifferentiableOn.neg, ModelWithCorners.mdifferentiableOn, mdifferentiableOn_univ, mdifferentiableOn_congr, FiberBundle.exists_mdifferentiableOn_extend, mdifferentiableOn_const, mdifferentiableOn_union_iff_of_isOpen, MDifferentiableOn.mul, MDifferentiableOn.union_of_isOpen, MDifferentiableOn.smul_section, IsLocalDiffeomorphOn.mdifferentiableOn, Bundle.mdifferentiableOn_zeroSection, ContinuousLinearMap.mdifferentiableOn, mdifferentiableOn_add_section, mdifferentiableOn_atlas_symm, mdifferentiableOn_iff_of_mem_maximalAtlas, mdifferentiableOn_neg_section, MDifferentiableOn.pow, MDifferentiable.mdifferentiableOn, mdifferentiableOn_iff_of_subset_source', MDifferentiableOn.clm_bundle_apply₂, ContMDiffOn.mdifferentiableOn
|
MDifferentiableWithinAt 📖 | MathDef | 116 mathmath: MDifferentiableAt.comp_mdifferentiableWithinAt, DifferentiableWithinAt.comp_mdifferentiableWithinAt, MDifferentiableWithinAt.add, mdifferentiableWithinAt_totalSpace, MDifferentiableWithinAt.snd, mdifferentiableWithinAt_iff_of_mem_maximalAtlas, MDifferentiableWithinAt.mul, mdifferentiableWithinAt_smul_const_section, MDifferentiableWithinAt.congr', mdifferentiableWithinAt_iff_target_inter, mdifferentiableWithinAt_congr_of_mem, MDifferentiableWithinAt.comp_of_eq, MDifferentiableWithinAt.finsum_section_of_locallyFinite, MDifferentiableAt.mdifferentiableWithinAt, mdifferentiableWithinAt_iff_exists_hasMFDerivWithinAt, mdifferentiableWithinAt_inter', mdifferentiableWithinAt_section, mdifferentiableWithinAt_univ, MDifferentiableWithinAt.prodMk_space, MDifferentiableWithinAt.clm_bundle_apply₂, MDifferentiableWithinAt.coordChange, mdifferentiableWithinAt_insert, mdifferentiableWithinAt_congr_nhds, mdifferentiableWithinAt_id, MDifferentiableWithinAt.cle_arrowCongr, MDifferentiableWithinAt.clm_precomp, MDifferentiableWithinAt.congr_of_eventuallyEq_insert, DifferentiableWithinAt.mdifferentiableWithinAt, HasMFDerivWithinAt.mdifferentiableWithinAt, mdifferentiableWithinAt_neg_section, Bundle.Trivialization.mdifferentiableWithinAt_totalSpace_iff, DifferentiableAt.comp_mdifferentiableWithinAt, MDifferentiableWithinAt.coordChangeL, MDifferentiableWithinAt.of_insert, MDifferentiableWithinAt.congr, mdifferentiableWithinAt_iff_image, MDifferentiableWithinAt.insert, MDifferentiableWithinAt.mpullbackWithin_vectorField_inter_of_eq, mdifferentiableWithinAt_of_isInvertible_mfderivWithin, mdifferentiableWithinAt_iff_differentiableWithinAt, MDifferentiableWithinAt.congr_of_mem, MDifferentiableWithinAt.clm_apply_of_inCoordinates, Bundle.mdifferentiableWithinAt_proj, MDifferentiableWithinAt.mono, MDifferentiableWithinAt.prodMk, mdifferentiableWithinAt_sub_section, mdifferentiableWithinAt_add_section, mdifferentiableWithinAt_const, MDifferentiableWithinAt.sum_section_of_locallyFinite, MDifferentiableWithinAt.congr_of_eventuallyEq, MDifferentiableWithinAt.inner_bundle, ContinuousLinearMap.mdifferentiableWithinAt, mdifferentiableWithinAt_iff', mdifferentiableWithinAt_inter, MDifferentiableWithinAt.congr_of_eventuallyEq_of_mem, mdifferentiableWithinAt_iff_target_inter', MDifferentiableWithinAt.clm_comp, Bundle.mdifferentiableWithinAt_zeroSection, ContinuousLinearEquiv.mdifferentiableWithinAt, mdifferentiableWithinAt_of_mfderivWithin_injective, mdifferentiableWithinAt_comp_projIcc_iff, mdifferentiableWithinAt_iff_of_mem_source', mdifferentiableWithinAt_iff_source_of_mem_maximalAtlas, mdifferentiableWithinAt_iff, Filter.EventuallyEq.mdifferentiablefWithinAt_iff, MDifferentiableWithinAt.comp, mdifferentiableWithinAt_snd, MDifferentiableWithinAt.mono_of_mem_nhdsWithin, MDifferentiableWithinAt.clm_postcomp, MDifferentiableWithinAt.comp_of_preimage_mem_nhdsWithin, MDifferentiableWithinAt.mpullback_vectorField_preimage, MDifferentiableWithinAt.clm_bundle_apply, mdifferentiableWithinAt_congr, ContMDiff.mdifferentiableWithinAt, Differentiable.comp_mdifferentiableWithinAt, ContMDiffWithinAt.mdifferentiableWithinAt, Filter.EventuallyEq.mdifferentiableWithinAt_iff, MDifferentiableWithinAt.fst, mdifferentiableAt_iff_source_of_mem_source, mdifferentiableWithinAt_iff_target_of_mem_source, MDifferentiableWithinAt.mpullbackWithin_vectorField_inter, mdifferentiableWithinAt_extChartAt_symm, mdifferentiableWithinAt_fst, mdifferentiableWithinAt_of_subsingleton, mdifferentiableWithinAt_iff_source_of_mem_source, MDifferentiableWithinAt.mpullback_vectorField_preimage_of_eq, mdifferentiableWithinAt_prod_module_iff, MDifferentiableWithinAt.prodMap, DifferentiableWithinAt.mdifferentiableWithinAt_of_comp_extChartAt_symm, mdifferentiableWithinAt_insert_self, mdifferentiableWithinAt_congr_set', mdifferentiableWithinAt_iff_of_mem_source, mdifferentiableWithinAt_congr_set, MDifferentiableWithinAt.insert', MDifferentiableWithinAt.congr_mono, Bundle.Trivialization.mdifferentiableWithinAt_section_iff, mdifferentiableWithinAt_prod_iff, MDifferentiableWithinAt.smul, MDifferentiableAt.comp_mdifferentiableWithinAt_of_eq, MDifferentiableWithinAt.pow, MDifferentiableWithinAt.comp_of_preimage_mem_nhdsWithin_of_eq, ModelWithCorners.mdifferentiableWithinAt_symm, MDifferentiableWithinAt.clm_prodMap, Bundle.Trivialization.mdifferentiableWithinAt_snd_comp_iff₂, MDifferentiableWithinAt.prodMap', mdifferentiableWithinAt_hom_bundle, MDifferentiableWithinAt.change_section_trivialization, MDifferentiableWithinAt.clm_apply, mdifferentiableWithinAt_iff_target, MDifferentiableWithinAt.congr_nhds, MDifferentiableWithinAt.prod, MDifferentiableWithinAt.sum_section, MDifferentiableWithinAt.sum, MDifferentiableWithinAt.smul_section, MDifferentiableWithinAt.neg, ModelWithCorners.mdifferentiableWithinAt
|
UniqueMDiffOn 📖 | MathDef | 16 mathmath: UniqueMDiffOn.uniqueMDiffOn_preimage, Diffeomorph.uniqueMDiffOn_preimage, UniqueMDiffOn.prod, UniqueMDiffOn.inter, UniqueMDiffOn.image_denseRange', IsOpen.uniqueMDiffOn, UniqueMDiffOn.uniqueMDiffOn_target_inter, UniqueMDiffOn.image_denseRange, uniqueMDiffOn_univ, Diffeomorph.uniqueMDiffOn_image, UniqueMDiffOn.tangentBundle_proj_preimage, ModelWithCorners.uniqueMDiffOn, Diffeomorph.uniqueMDiffOn_image_aux, uniqueMDiffOn_iff_uniqueDiffOn, UniqueMDiffOn.bundle_preimage, UniqueDiffOn.uniqueMDiffOn
|
UniqueMDiffWithinAt 📖 | MathDef | 16 mathmath: UniqueMDiffWithinAt.mono_of_mem_nhdsWithin, UniqueMDiffWithinAt.inter', UniqueMDiffWithinAt.inter, UniqueDiffWithinAt.uniqueMDiffWithinAt, UniqueMDiffWithinAt.bundle_preimage', UniqueMDiffWithinAt.preimage_openPartialHomeomorph, UniqueMDiffWithinAt.mono_nhds, uniqueMDiffWithinAt_univ, uniqueMDiffWithinAt_iff, UniqueMDiffWithinAt.bundle_preimage, UniqueMDiffWithinAt.mono, uniqueMDiffWithinAt_iff_inter_range, IsOpen.uniqueMDiffWithinAt, uniqueMDiffWithinAt_iff_uniqueDiffWithinAt, UniqueMDiffWithinAt.prod, UniqueMDiffWithinAt.image_denseRange
|
mfderiv 📖 | CompOp | 95 mathmath: mfderiv_sumSwap, mfderiv_prod_eq_add, Manifold.pathELength_eq_lintegral_mfderiv_Ioo, MDifferentiableAt.mfderiv_prod, tangentMap_snd, mfderiv_comp, SmoothBumpCovering.exists_immersion_euclidean, mfderiv_comp_apply_of_eq, VectorField.mlieBracket_smul_left, hasMFDerivAt_extChartAt, mfderiv_comp_of_eq, inTangentCoordinates_eq_mfderiv_comp, ContMDiffAt.mfderiv_apply, mfderivWithin_comp_projIcc_one, Manifold.pathELength_def, fromTangentSpace_mfderiv_smul_apply, HasMFDerivAt.mfderiv, MDifferentiableAt.hasMFDerivAt, mfderiv_prod_eq_add_comp, mfderiv_comp_mfderivWithin, hasMFDerivWithinAt_extChartAt, mfderiv_chartAt_eq_tangentCoordChange, mfderiv_sumInl, mfderiv_sub, ContMDiffAt.mfderiv_const, mfderiv_prodMap, mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm, Diffeomorph.mfderivToContinuousLinearEquiv_coe, HasMFDerivAt.prodMap, mfderivWithin_of_mem_nhds, VectorField.mpullback_apply, fromTangentSpace_mfderiv_smul', fromTangentSpace_mfderiv_smul_apply', mfderivWithin_univ, mfderiv_coe_sphere_injective, mfderiv_add, mfderivWithin_eq_mfderiv, ContinuousLinearMap.mfderiv_eq, mfderiv_extChartAt_self, OpenPartialHomeomorph.MDifferentiable.comp_symm_deriv, SmoothBumpCovering.embeddingPiTangent_injective_mfderiv, MDifferentiableAt.mfderiv, OpenPartialHomeomorph.MDifferentiable.mfderiv_bijective, MDifferentiable.mfderivWithin, mfderiv_prod_right, SmoothBumpCovering.embeddingPiTangent_ker_mfderiv, Manifold.riemannianEDist_def, OpenPartialHomeomorph.MDifferentiable.range_mfderiv_eq_top, TangentBundle.continuousLinearMapAt_trivializationAt, IsLocalDiffeomorph.mfderivToContinuousLinearEquiv_coe, OpenPartialHomeomorph.MDifferentiable.mfderiv_surjective, eventually_enorm_mfderiv_extChartAt_lt, fromTangentSpace_mfderiv_smul, mfderiv_sumInr, mfderiv_snd, mfderiv_zero_of_not_mdifferentiableAt, range_mfderiv_coe_sphere, mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm', SmoothBumpCovering.comp_embeddingPiTangent_mfderiv, ContinuousLinearEquiv.mfderiv_eq, mfderiv_prodMk, mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt', mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt, mfderiv_comp_apply, OpenPartialHomeomorph.MDifferentiable.symm_comp_deriv, VectorField.mfderiv_extChartAt_inverse_comp_mfderivWithin_extChartAT_symm, Manifold.pathELength_eq_lintegral_mfderiv_Icc, OpenPartialHomeomorph.MDifferentiable.mfderiv_injective, mfderiv_const, inverse_mfderiv_mul_left, ContMDiffAt.mfderiv, Filter.EventuallyEq.mfderiv_eq, exists_embedding_euclidean_of_compact, Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc, OpenPartialHomeomorph.MDifferentiable.ker_mfderiv_eq_bot, mfderiv_smul, isInvertible_mfderiv_extChartAt, mfderivWithin_of_isOpen, OpenPartialHomeomorph.MDifferentiable.range_mfderiv_eq_univ, mfderiv_eq_fderiv, mfderiv_fst, VectorField.mlieBracketWithin_apply, mfderiv_subtype_coe_Icc_one, mfderiv_neg, IsLocalDiffeomorphAt.mfderivToContinuousLinearEquiv_coe, mfderiv_congr_point, mfderiv_prod_left, eventually_norm_mfderiv_extChartAt_lt, mfderiv_comp_mfderivWithin_of_eq, mfderiv_congr, inverse_mfderiv_add_left, const_smul_mfderiv, mfderiv_prod_eq_add_apply, VectorField.mlieBracket_smul_right, mfderiv_id
|
mfderivWithin 📖 | CompOp | 66 mathmath: MDifferentiableWithinAt.hasMFDerivWithinAt, mfderivWithin_congr_set, mfderivWithin_range_extChartAt_symm, eventually_enorm_mfderivWithin_symm_extChartAt_lt, TangentBundle.symmL_trivializationAt, ContMDiffWithinAt.mfderivWithin_const, inTangentCoordinates_eq_mfderiv_comp, mfderivWithin_projIcc_one, mfderivWithin_comp_projIcc_one, mfderivWithin_congr_of_mem, eventually_norm_mfderivWithin_symm_extChartAt_lt, Manifold.pathELength_eq_lintegral_mfderivWithin_Icc, mfderivWithin_sumInr, mfderivWithin_comp_of_preimage_mem_nhdsWithin_of_eq, mfderiv_comp_mfderivWithin, tangentMapWithin_snd, mfderivWithin_sumInl, HasMFDerivWithinAt.mfderivWithin, mfderivWithin_extChartAt_symm_inverse_apply, mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm, mfderivWithin_of_mem_nhds, mfderivWithin_eventually_congr_set', mfderivWithin_univ, mfderivWithin_eq_mfderiv, Filter.EventuallyEq.mfderivWithin_eq_of_mem, mfderivWithin_comp_of_preimage_mem_nhdsWithin, VectorField.mlieBracketWithin_smul_left, Filter.EventuallyEq.mfderivWithin_eq, MDifferentiableWithinAt.mfderivWithin_congr_mono, MDifferentiableWithinAt.mfderivWithin, VectorField.mlieBracketWithin_smul_right, MDifferentiable.mfderivWithin, mfderivWithin_zero_of_not_mdifferentiableWithinAt, ContMDiffWithinAt.mfderivWithin, mfderivWithin_const, mfderivWithin_eq_fderivWithin, oneTangentSpaceIcc_def, mfderivWithin_prodMap, ContMDiffWithinAt.mfderivWithin_apply, ContinuousLinearMap.mfderivWithin_eq, mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm', mfderivWithin_congr_set', mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt', mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt, VectorField.mpullback_mfderivWithin_apply_smul, VectorField.mfderiv_extChartAt_inverse_comp_mfderivWithin_extChartAT_symm, mfderivWithin_inter, mfderivWithin_prodMk, mfderivWithin_eventually_congr_set, VectorField.mpullbackWithin_apply, eventually_norm_mfderivWithin_symm_extChartAt_comp_lt, MDifferentiableWithinAt.mfderivWithin_mono, mfderivWithin_subset, mfderivWithin_of_isOpen, mfderivWithin_fst, mfderivWithin_congr, isInvertible_mfderivWithin_extChartAt_symm, MDifferentiableWithinAt.mfderivWithin_mono_of_mem_nhdsWithin, mfderivWithin_id, mfderivWithin_sumSwap, mfderiv_comp_mfderivWithin_of_eq, mfderivWithin_snd, mfderivWithin_comp, HasMFDerivWithinAt.mfderivWithin_eq_zero, ContinuousLinearEquiv.mfderivWithin_eq, mfderivWithin_comp_of_eq
|
tangentMap 📖 | CompOp | 17 mathmath: TangentBundle.tangentMap_tangentBundle_pure, tangentMap_snd, tangentMap_chart, ContMDiff.contMDiff_tangentMap, tangentMap_prodSnd, tangentMap_id, tangentMap_chart_symm, tangentMap_comp, tangentMap_comp_at, tangentMapWithin_univ, tangentMap_proj, equivTangentBundleProd_eq_tangentMap_prod_tangentMap, tangentMap_prodFst, tangentMapWithin_eq_tangentMap, tangentMap_prod_right, tangentMap_prod_left, ContMDiff.continuous_tangentMap
|
tangentMapWithin 📖 | CompOp | 12 mathmath: tangentMapWithin_congr, tangentMapWithin_prodSnd, tangentMapWithin_subset, tangentMapWithin_snd, tangentMapWithin_proj, ContMDiffOn.continuousOn_tangentMapWithin, tangentMapWithin_prodFst, tangentMapWithin_comp_at, tangentMapWithin_univ, ContMDiffOn.contMDiffOn_tangentMapWithin, tangentMapWithin_eq_tangentMap, tangentMapWithin_id
|