| Name | Category | Theorems |
|---|
DifferentiableWithinAtProp 📖 | MathDef | 4 mathmath: differentiableWithinAtProp_self_source, DifferentiableWithinAtProp_self, differentiableWithinAt_localInvariantProp, differentiableWithinAtProp_self_target
|
HasMFDerivAt 📖 | MathDef | 18 mathmath: hasMFDerivAt_extChartAt, hasMFDerivAt_sumSwap, hasMFDerivAt_fst, ModelWithCorners.hasMFDerivAt, hasMFDerivAt_inr, MDifferentiableAt.hasMFDerivAt, hasMFDerivAt_neg, ContinuousLinearEquiv.hasMFDerivAt, HasFDerivAt.hasMFDerivAt, hasMFDerivAt_id, hasMFDerivAt_inl, IsMIntegralCurveAt.hasMFDerivAt, hasMFDerivAt_const, ContinuousLinearMap.hasMFDerivAt, hasMFDerivWithinAt_univ, hasMFDerivAt_iff_hasFDerivAt, hasMFDerivAt_snd, HasMFDerivWithinAt.hasMFDerivAt
|
HasMFDerivWithinAt 📖 | MathDef | 23 mathmath: MDifferentiableWithinAt.hasMFDerivWithinAt, hasMFDerivWithinAt_insert, mdifferentiableWithinAt_iff_exists_hasMFDerivWithinAt, hasMFDerivWithinAt_diff_singleton, ContinuousLinearEquiv.hasMFDerivWithinAt, hasMFDerivWithinAt_extChartAt, hasMFDerivWithinAt_inr, hasMFDerivWithinAt_id, hasMFDerivWithinAt_fst, hasMFDerivWithinAt_inter', ModelWithCorners.hasMFDerivWithinAt, HasFDerivWithinAt.hasMFDerivWithinAt, hasMFDerivWithinAt_const, ModelWithCorners.hasMFDerivWithinAt_symm, hasMFDerivWithinAt_univ, HasMFDerivAt.hasMFDerivWithinAt, hasMFDerivWithinAt_snd, hasMFDerivWithinAt_congr_set, hasMFDerivWithinAt_inter, ContinuousLinearMap.hasMFDerivWithinAt, hasMFDerivWithinAt_inl, hasMFDerivWithinAt_iff_hasFDerivWithinAt, hasMFDerivWithinAt_congr_set'
|
MDifferentiableAt 📖 | MathDef | 53 mathmath: Bundle.mdifferentiableAt_proj, Trivialization.mdifferentiableAt_section_iff, MDifferentiable.mdifferentiableAt, ContMDiffAt.mdifferentiableAt, mdifferentiableWithinAt_univ, MDifferentiableOn.mdifferentiableAt, IsLocalDiffeomorphAt.localInverse_mdifferentiableAt, OpenPartialHomeomorph.MDifferentiable.mdifferentiableAt_symm, mdifferentiableAt_iff, mdifferentiableAt_addInvariantVectorField, mdifferentiableAt_mul_right, mdifferentiableAt_fst, mdifferentiableAt_totalSpace, Trivialization.mdifferentiableAt_totalSpace_iff, mdifferentiableAt_hom_bundle, mdifferentiableAt_snd, mdifferentiableAt_add_right, mdifferentiableAt_prod_module_iff, ModelWithCorners.mdifferentiableAt, mdifferentiableAt_mul_left, mdifferentiableAt_add_left, mdifferentiableAt_iff_target_of_mem_source, HasMFDerivAt.mdifferentiableAt, mdifferentiableAt_prod_iff, mdifferentiableAt_of_isInvertible_mfderiv, IsLocalDiffeomorphAt.mdifferentiableAt, mdifferentiableAt_neg, MDifferentiableWithinAt.mdifferentiableAt, mdifferentiableWithinAt_comp_projIcc_iff, mdifferentiableAt_section, mdifferentiableAt_const, 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_iff_target, ContMDiffSection.mdifferentiableAt, UpperHalfPlane.mdifferentiableAt_iff, DifferentiableAt.mdifferentiableAt, ContMDiff.mdifferentiableAt, mdifferentiableAt_atlas, Bundle.mdifferentiableAt_zeroSection, ContinuousLinearEquiv.mdifferentiableAt, mdifferentiableAt_extChartAt, Filter.EventuallyEq.mdifferentiableAt_iff, UpperHalfPlane.mdifferentiableAt_ofComplex, ContinuousLinearMap.mdifferentiableAt
|
MDifferentiableOn 📖 | MathDef | 40 mathmath: mdifferentiableOn_iff, mdifferentiable_iff_target, mdifferentiableOn_empty, Trivialization.mdifferentiableOn_section_baseSet_iff, mdifferentiableOn_extChartAt, mdifferentiableOn_symm_coordChangeL, ModelWithCorners.mdifferentiableOn_symm, mdifferentiableOn_snd, mdifferentiableOn_id, Diffeomorph.mdifferentiableOn, mdifferentiableOn_iff_target, mdifferentiableOn_fst, mdifferentiableOn_prod_module_iff, mdifferentiableOn_iUnion_iff_of_isOpen, mdifferentiableOn_extChartAt_symm, DifferentiableOn.mdifferentiableOn, ContinuousLinearEquiv.mdifferentiableOn, mdifferentiableOn_iff_of_subset_source, Bundle.mdifferentiableOn_proj, mdifferentiableOn_continuousLinearMapCoordChange, PartialDiffeomorph.mdifferentiableOn, mdifferentiableOn_atlas, mdifferentiableOn_iff_of_mem_maximalAtlas', mdifferentiableOn_iff_differentiableOn, mdifferentiableOn_coordChangeL, mdifferentiableOn_prod_iff, Trivialization.mdifferentiableOn_section_iff, ModelWithCorners.mdifferentiableOn, mdifferentiableOn_univ, mdifferentiableOn_congr, mdifferentiableOn_const, mdifferentiableOn_union_iff_of_isOpen, IsLocalDiffeomorphOn.mdifferentiableOn, Bundle.mdifferentiableOn_zeroSection, ContinuousLinearMap.mdifferentiableOn, mdifferentiableOn_atlas_symm, mdifferentiableOn_iff_of_mem_maximalAtlas, MDifferentiable.mdifferentiableOn, mdifferentiableOn_iff_of_subset_source', ContMDiffOn.mdifferentiableOn
|
MDifferentiableWithinAt 📖 | MathDef | 52 mathmath: mdifferentiableWithinAt_totalSpace, mdifferentiableWithinAt_iff_of_mem_maximalAtlas, mdifferentiableWithinAt_iff_target_inter, mdifferentiableWithinAt_congr_of_mem, MDifferentiableAt.mdifferentiableWithinAt, mdifferentiableWithinAt_iff_exists_hasMFDerivWithinAt, mdifferentiableWithinAt_inter', mdifferentiableWithinAt_section, mdifferentiableWithinAt_univ, mdifferentiableWithinAt_insert, mdifferentiableWithinAt_congr_nhds, mdifferentiableWithinAt_id, DifferentiableWithinAt.mdifferentiableWithinAt, HasMFDerivWithinAt.mdifferentiableWithinAt, mdifferentiableWithinAt_iff_image, mdifferentiableWithinAt_of_isInvertible_mfderivWithin, mdifferentiableWithinAt_iff_differentiableWithinAt, Bundle.mdifferentiableWithinAt_proj, mdifferentiableWithinAt_const, ContinuousLinearMap.mdifferentiableWithinAt, mdifferentiableWithinAt_iff', mdifferentiableWithinAt_inter, mdifferentiableWithinAt_iff_target_inter', Bundle.mdifferentiableWithinAt_zeroSection, ContinuousLinearEquiv.mdifferentiableWithinAt, mdifferentiableWithinAt_comp_projIcc_iff, mdifferentiableWithinAt_iff_of_mem_source', mdifferentiableWithinAt_iff_source_of_mem_maximalAtlas, mdifferentiableWithinAt_iff, Trivialization.mdifferentiableWithinAt_section_iff, Filter.EventuallyEq.mdifferentiablefWithinAt_iff, mdifferentiableWithinAt_snd, mdifferentiableWithinAt_congr, ContMDiff.mdifferentiableWithinAt, ContMDiffWithinAt.mdifferentiableWithinAt, Filter.EventuallyEq.mdifferentiableWithinAt_iff, mdifferentiableAt_iff_source_of_mem_source, mdifferentiableWithinAt_iff_target_of_mem_source, mdifferentiableWithinAt_extChartAt_symm, mdifferentiableWithinAt_fst, mdifferentiableWithinAt_iff_source_of_mem_source, mdifferentiableWithinAt_prod_module_iff, Trivialization.mdifferentiableWithinAt_totalSpace_iff, mdifferentiableWithinAt_insert_self, mdifferentiableWithinAt_congr_set', mdifferentiableWithinAt_iff_of_mem_source, mdifferentiableWithinAt_congr_set, mdifferentiableWithinAt_prod_iff, ModelWithCorners.mdifferentiableWithinAt_symm, mdifferentiableWithinAt_hom_bundle, mdifferentiableWithinAt_iff_target, ModelWithCorners.mdifferentiableWithinAt
|
UniqueMDiffOn 📖 | MathDef | 7 mathmath: Diffeomorph.uniqueMDiffOn_preimage, IsOpen.uniqueMDiffOn, uniqueMDiffOn_univ, Diffeomorph.uniqueMDiffOn_image, ModelWithCorners.uniqueMDiffOn, uniqueMDiffOn_iff_uniqueDiffOn, UniqueDiffOn.uniqueMDiffOn
|
UniqueMDiffWithinAt 📖 | MathDef | 6 mathmath: UniqueDiffWithinAt.uniqueMDiffWithinAt, uniqueMDiffWithinAt_univ, uniqueMDiffWithinAt_iff, uniqueMDiffWithinAt_iff_inter_range, IsOpen.uniqueMDiffWithinAt, uniqueMDiffWithinAt_iff_uniqueDiffWithinAt
|
mfderiv 📖 | CompOp | 86 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, hasMFDerivAt_extChartAt, mfderiv_comp_of_eq, inTangentCoordinates_eq_mfderiv_comp, ContMDiffAt.mfderiv_apply, mfderivWithin_comp_projIcc_one, Manifold.pathELength_def, 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, mfderivWithin_univ, mfderiv_coe_sphere_injective, mfderiv_add, mfderivWithin_eq_mfderiv, ContinuousLinearMap.mfderiv_eq, 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, 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, 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, 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, mfderiv_id
|
mfderivWithin 📖 | CompOp | 60 mathmath: MDifferentiableWithinAt.hasMFDerivWithinAt, mfderivWithin_congr_set, 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, 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, Filter.EventuallyEq.mfderivWithin_eq, MDifferentiableWithinAt.mfderivWithin_congr_mono, MDifferentiableWithinAt.mfderivWithin, 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, 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
|