Defs

📁 Source: Mathlib/Geometry/Manifold/ContMDiff/Defs.lean

Statistics

Metric	Count
Definitions ContDiffWithinAtProp, ContMDiff, ContMDiffAt, ContMDiffOn, ContMDiffWithinAt	5
Theorems contMDiffAt, contMDiffOn, continuous, of_le, of_succ, congr_of_eventuallyEq, contMDiffWithinAt, continuousAt, of_le, of_succ, congr_mono, contMDiffAt, continuousOn, mono, of_le, of_succ, congr', congr_of_eventuallyEq, congr_of_eventuallyEq_of_mem, congr_of_mem, congr_set, contMDiffAt, contMDiffOn, contMDiffOn', continuousWithinAt, insert, mono, mono_of_mem_nhdsWithin, of_insert, of_le, of_succ, contMDiffAt_iff, contMDiffWithinAt_iff, contDiffWithinAtProp_id, contDiffWithinAtProp_mono_of_mem_nhdsWithin, contDiffWithinAtProp_self, contDiffWithinAtProp_self_source, contDiffWithinAtProp_self_target, contDiffWithinAt_localInvariantProp, contDiffWithinAt_localInvariantProp_of_le, contMDiffAt_iff, contMDiffAt_iff_contMDiffAt_nhds, contMDiffAt_iff_contMDiffOn_nhds, contMDiffAt_iff_le_ne_infty, contMDiffAt_iff_nat, contMDiffAt_iff_of_mem_source, contMDiffAt_iff_source, contMDiffAt_iff_source_of_mem_source, contMDiffAt_iff_target, contMDiffAt_iff_target_of_mem_source, contMDiffAt_infty, contMDiffOn_congr, contMDiffOn_empty, contMDiffOn_iff, contMDiffOn_iff_of_mem_maximalAtlas, contMDiffOn_iff_of_mem_maximalAtlas', contMDiffOn_iff_of_subset_source, contMDiffOn_iff_of_subset_source', contMDiffOn_iff_source_of_mem_maximalAtlas, contMDiffOn_iff_target, contMDiffOn_infty, contMDiffOn_of_locally_contMDiffOn, contMDiffOn_univ, contMDiffOn_zero_iff, contMDiffWithinAt_congr, contMDiffWithinAt_congr_of_mem, contMDiffWithinAt_congr_set, contMDiffWithinAt_congr_set', contMDiffWithinAt_iff, contMDiffWithinAt_iff', contMDiffWithinAt_iff_contMDiffOn_nhds, contMDiffWithinAt_iff_contMDiffWithinAt_nhdsWithin, contMDiffWithinAt_iff_image, contMDiffWithinAt_iff_le_ne_infty, contMDiffWithinAt_iff_nat, contMDiffWithinAt_iff_of_mem_maximalAtlas, contMDiffWithinAt_iff_of_mem_source, contMDiffWithinAt_iff_of_mem_source', contMDiffWithinAt_iff_source, contMDiffWithinAt_iff_source_of_mem_maximalAtlas, contMDiffWithinAt_iff_source_of_mem_source, contMDiffWithinAt_iff_target, contMDiffWithinAt_iff_target_of_mem_source, contMDiffWithinAt_infty, contMDiffWithinAt_insert_self, contMDiffWithinAt_inter, contMDiffWithinAt_inter', contMDiffWithinAt_univ, contMDiff_congr, contMDiff_iff, contMDiff_iff_target, contMDiff_infty, contMDiff_of_locally_contMDiffOn, contMDiff_zero_iff	94
Total	99

ContMDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contMDiffAt 📖	mathematical	ContMDiff	ContMDiffAt	—	—
contMDiffOn 📖	mathematical	ContMDiff	ContMDiffOn	—	ContMDiffAt.contMDiffWithinAt
continuous 📖	mathematical	ContMDiff	Continuous	—	continuous_iff_continuousAt ContMDiffAt.continuousAt
of_le 📖	—	ContMDiff WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat	—	—	ContMDiffAt.of_le
of_succ 📖	—	ContMDiff WithTop ENat WithTop.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—	ContMDiffAt.of_succ

ContMDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_of_eventuallyEq 📖	—	ContMDiffAt Filter.EventuallyEq nhds	—	—	StructureGroupoid.LocalInvariantProp.liftPropAt_congr_of_eventuallyEq contDiffWithinAt_localInvariantProp
contMDiffWithinAt 📖	mathematical	ContMDiffAt	ContMDiffWithinAt	—	ContMDiffWithinAt.mono Set.subset_univ
continuousAt 📖	mathematical	ContMDiffAt	ContinuousAt	—	continuousWithinAt_univ ContMDiffWithinAt.continuousWithinAt
of_le 📖	—	ContMDiffAt WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat	—	—	ContMDiffWithinAt.of_le
of_succ 📖	—	ContMDiffAt WithTop ENat WithTop.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—	ContMDiffWithinAt.of_succ

ContMDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_mono 📖	—	ContMDiffOn Set Set.instHasSubset	—	—	congr mono
contMDiffAt 📖	mathematical	ContMDiffOn Set Filter Filter.instMembership nhds	ContMDiffAt	—	ContMDiffWithinAt.contMDiffAt mem_of_mem_nhds
continuousOn 📖	mathematical	ContMDiffOn	ContinuousOn	—	ContMDiffWithinAt.continuousWithinAt
mono 📖	—	ContMDiffOn Set Set.instHasSubset	—	—	ContMDiffWithinAt.mono
of_le 📖	—	ContMDiffOn WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat	—	—	ContMDiffWithinAt.of_le
of_succ 📖	—	ContMDiffOn WithTop ENat WithTop.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—	ContMDiffWithinAt.of_succ

ContMDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr' 📖	—	ContMDiffWithinAt Set Set.instHasSubset Set.instMembership	—	—	congr
congr_of_eventuallyEq 📖	—	ContMDiffWithinAt Filter.EventuallyEq nhdsWithin	—	—	StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_of_eventuallyEq contDiffWithinAt_localInvariantProp
congr_of_eventuallyEq_of_mem 📖	—	ContMDiffWithinAt Filter.EventuallyEq nhdsWithin Set Set.instMembership	—	—	StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_of_eventuallyEq_of_mem contDiffWithinAt_localInvariantProp
congr_of_mem 📖	—	ContMDiffWithinAt Set Set.instMembership	—	—	StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_of_mem contDiffWithinAt_localInvariantProp
congr_set 📖	—	ContMDiffWithinAt Filter.EventuallyEq nhds	—	—	contMDiffWithinAt_congr_set
contMDiffAt 📖	mathematical	ContMDiffWithinAt Set Filter Filter.instMembership nhds	ContMDiffAt	—	StructureGroupoid.LocalInvariantProp.liftPropAt_of_liftPropWithinAt contDiffWithinAt_localInvariantProp
contMDiffOn 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat Top.top WithTop.top ContMDiffWithinAt	Set Filter Filter.instMembership nhdsWithin Set.instInsert Set.instHasSubset ContMDiffOn	—	contMDiffOn' inter_mem_nhdsWithin IsOpen.mem_nhds Set.inter_subset_left
contMDiffOn' 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat Top.top WithTop.top ContMDiffWithinAt	IsOpen Set Set.instMembership ContMDiffOn Set.instInter Set.instInsert	—	IsManifold.of_le contMDiffWithinAt_iff_contMDiffOn_nhds of_le mem_nhdsWithin ContMDiffOn.mono Set.inter_comm ContMDiffOn.of_le
continuousWithinAt 📖	mathematical	ContMDiffWithinAt	ContinuousWithinAt	—	ChartedSpace.LiftPropWithinAt.continuousWithinAt
insert 📖	mathematical	ContMDiffWithinAt	Set Set.instInsert	—	contMDiffWithinAt_insert_self
mono 📖	—	ContMDiffWithinAt Set Set.instHasSubset	—	—	mono_of_mem_nhdsWithin Filter.mem_of_superset self_mem_nhdsWithin
mono_of_mem_nhdsWithin 📖	—	ContMDiffWithinAt Set Filter Filter.instMembership nhdsWithin	—	—	StructureGroupoid.LocalInvariantProp.liftPropWithinAt_mono_of_mem_nhdsWithin contDiffWithinAtProp_mono_of_mem_nhdsWithin
of_insert 📖	—	ContMDiffWithinAt Set Set.instInsert	—	—	contMDiffWithinAt_insert_self
of_le 📖	—	ContMDiffWithinAt WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat	—	—	ChartedSpace.LiftPropWithinAt.continuousWithinAt ContDiffWithinAt.of_le ChartedSpace.LiftPropWithinAt.prop
of_succ 📖	—	ContMDiffWithinAt WithTop ENat WithTop.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—	of_le le_self_add WithTop.canonicallyOrderedAdd

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contMDiffAt_iff 📖	mathematical	Filter.EventuallyEq nhds	ContMDiffAt	—	StructureGroupoid.LocalInvariantProp.liftPropAt_congr_iff_of_eventuallyEq contDiffWithinAt_localInvariantProp
contMDiffWithinAt_iff 📖	mathematical	Filter.EventuallyEq nhdsWithin	ContMDiffWithinAt	—	StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff_of_eventuallyEq contDiffWithinAt_localInvariantProp

(root)

Definitions

Name	Category	Theorems
ContDiffWithinAtProp 📖	MathDef	10 math math: contDiffWithinAtProp_self, smoothSheafCommRing.eval_germ, contDiffWithinAtProp_id, smoothSheafCommRing.evalHom_germ, contDiffWithinAtProp_self_source, contDiffWithinAt_localInvariantProp, contDiffWithinAt_localInvariantProp_of_le, contDiffWithinAtProp_self_target, smoothSheaf.eval_germ, smoothSheaf.contMDiff_section
ContMDiff 📖	MathDef	108 math math: contMDiff_prod_assoc, contMDiff_congr, Bundle.ContMDiffRiemannianMetric.contMDiff, contMDiff_addInvariantVectorField, contMDiff_neg_sphere, SmoothBumpCovering.exists_immersion_euclidean, IsOpen.exists_msmooth_support_eq, ContMDiffMul.contMDiff_mul, contMDiff_mul, contMDiff_mulInvariantVectorField, contMDiff_sum_map, contMDiff_equivTangentBundleProd_symm, contMDiff_add_right, contMDiff_inclusion, ContinuousLinearMap.contMDiff, contMDiff_mul_right, contMDiff_infty, ContMDiffMonoidMorphism.contMDiff_toFun, Trivialization.contMDiff_iff, contMDiff_pow, ContMDiffAdd.contMDiff_add, Diffeomorph.contMDiff_comp_diffeomorph_iff, ContMDiff.inr, Diffeomorph.contMDiff_toFun, contMDiff_mul_left, UpperHalfPlane.contMDiff_coe, contMDiff_coe_sphere, IsOpen.exists_contMDiff_support_eq_aux, contMDiff_isOpenEmbedding, contMDiff_model, UpperHalfPlane.contMDiff_inv_denom, contMDiff_of_discreteTopology, contMDiff_zero_iff, ContMDiff.inl, contMDiff_vectorSpace_iff_contDiff, IsLocalDiffeomorph.contMDiff, IsContMDiffRiemannianBundle.exists_contMDiff, contMDiff_snd, contMDiff_subtype_coe_Icc, contMDiff_const, contMDiff_iff_contDiff, contMDiff_iff_target, UpperHalfPlane.contMDiff_num, ContMDiffMap.contMDiff, ContMDiff.swap, contMDiff_of_tsupport, IsOpen.exists_contMDiff_support_eq, contMDiff_smul, contMDiff_of_contMDiffOn_union_of_isOpen, contMDiff_neg, contMDiff_of_mulTSupport, exists_msmooth_support_eq_eq_one_iff, LieGroup.contMDiff_inv, exists_msmooth_zero_iff_one_iff_of_isClosed, ContMDiffRing.contMDiff_mul, contMDiff_prod_iff, ContDiff.contMDiff, Manifold.riemannianEDist_def, contMDiff_one, UpperHalfPlane.contMDiff_denom_zpow, 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, ContMDiffAddMonoidMorphism.contMDiff_toFun, contMDiff_of_contMDiffOn_iUnion_of_isOpen, Bundle.contMDiff_zeroSection, contMDiff_prod_module_iff, contMDiffOn_univ, contMDiff_id, exists_contMDiff_support_eq_eq_one_iff, ContMDiffSection.contMDiff, contMDiff_equivTangentBundleProd, SmoothPartitionOfUnity.contMDiff_finsum_smul, contMDiff_zero, contMDiffOn_comp_projIcc_iff, SmoothBumpFunction.contMDiff, smoothSheaf.contMDiff_section, contMDiff_add, contMDiff_of_locally_contMDiffOn, exists_embedding_euclidean_of_compact, ContinuousLinearEquiv.contMDiff_transContinuousLinearEquiv_left, Units.contMDiff_val, contMDiff_tangentBundleModelSpaceHomeomorph, ContMDiffOn.smul_section_of_tsupport, contMDiff_pi_space, contMDiff_nsmul, Diffeomorph.contMDiff_diffeomorph_comp_iff, contMDiff_tangentBundleModelSpaceHomeomorph_symm, contMDiff_of_subsingleton, Diffeomorph.contMDiff, SmoothPartitionOfUnity.contMDiff_smul, UpperHalfPlane.contMDiff_smul, UpperHalfPlane.contMDiff_denom, ContMDiffSection.contMDiff_toFun, SmoothPartitionOfUnity.IsSubordinate.contMDiff_finsum_smul, contMDiff_fst, Manifold.exists_lt_locally_constant_of_riemannianEDist_lt, contMDiff_snd_tangentBundle_modelSpace, contMDiff_subtype_val, SmoothPartitionOfUnity.contMDiff_sum, contMDiff_add_left, contMDiff_circleExp
ContMDiffAt 📖	MathDef	68 math math: contMDiffAt_add_right, contMDiffAt_extend, ContinuousLinearEquiv.contMDiffAt_transContinuousLinearEquiv_right, contMDiffAt_iff_of_mem_source, ContDiffAt.contMDiffAt, contMDiffAt_iff_source, contMDiffAt_iff_le_ne_infty, Trivialization.contMDiffAt_iff, Bundle.contMDiffAt_zeroSection, contMDiffAt_mulInvariantVectorField, contMDiffAt_add_left, contMDiffAt_const, ContinuousLinearEquiv.contMDiffAt_transContinuousLinearEquiv_left, contMDiffAt_iff_source_of_mem_source, ContMDiffWithinAt.contMDiffAt, contMDiffAt_iff_contMDiffOn_nhds, SmoothBumpFunction.contMDiffAt, contMDiffAt_prod_iff, contMDiffAt_coordChangeL, ContMDiffInv₀.contMDiffAt_inv₀, Diffeomorph.contMDiffAt_diffeomorph_comp_iff, contMDiffAt_iff, contMDiffAt_of_notMem, contMDiffAt_iff_contMDiffAt_nhds, IsLocalFrameOn.contMDiffAt, contMDiffAt_hom_bundle, contMDiffAt_id, contMDiffAt_one, Bundle.contMDiffAt_totalSpace, Diffeomorph.contMDiffAt_comp_diffeomorph_iff, contMDiffWithinAt_comp_projIcc_iff, contMDiffAt_iff_nat, Filter.EventuallyEq.contMDiffAt_iff, contMDiffAt_iff_target_of_mem_source, contMDiffAt_section_of_mem_baseSet, IsLocalDiffeomorphAt.localInverse_contMDiffAt, contMDiffAt_vectorSpace_iff_contDiffAt, contMDiffAt_extChartAt, ContMDiffOn.contMDiffAt, contMDiffAt_symm_of_mem_maximalAtlas, contMDiffAt_localFrame_of_mem, Diffeomorph.contMDiffAt, contMDiffAt_subtype_iff, Bundle.contMDiffAt_section, contMDiffAt_prod_module_iff, contMDiffWithinAt_univ, UpperHalfPlane.contMDiffAt_ofComplex, Trivialization.contMDiffAt_section_iff, UpperHalfPlane.contMDiffAt_iff, contMDiffAt_of_mem_maximalAtlas, Bundle.contMDiffAt_proj, contMDiffAt_addInvariantVectorField, contMDiffAt_extChartAt', contMDiffAt_infty, ContMDiff.contMDiffAt, contMDiffAt_mul_right, contMDiffAt_of_subsingleton, contMDiffAt_mul_left, contMDiffAt_fst, contMDiffAt_inv₀, contMDiffAt_pi_space, contMDiffAt_iff_target, IsLocalDiffeomorphAt.contMDiffAt, ContinuousLinearMap.contMDiffAt, contMDiffAt_iff_contDiffAt, contMDiffAt_snd, contMDiffAt_zero, contMDiffAt_of_notMem_mulTSupport
ContMDiffOn 📖	MathDef	80 math math: contMDiffOn_of_subsingleton, Bundle.contMDiffOn_zeroSection, Diffeomorph.contMDiffOn_comp_diffeomorph_iff, PartialDiffeomorph.contMDiffOn, contMDiffOn_chart, VectorBundleCore.contMDiffOn_coordChange, contMDiffOn_chart_symm, Trivialization.contMDiffOn_symm_trans, PartialDiffeomorph.contMDiffOn_toFun, contMDiffOn_isOpenEmbedding_symm, Trivialization.contMDiffOn_section_iff, contMDiffOn_inv₀, contMDiffOn_iff_contDiffOn, ContDiffOn.contMDiffOn, IsLocalDiffeomorphAt.localInverse_contMDiffOn, contMDiffOn_pi_space, contMDiffAt_iff_contMDiffOn_nhds, contMDiffOn_zero, contMDiff_iff_target, contMDiffOn_extChartAt, ContMDiff.contMDiffOn, Trivialization.contMDiffOn_localFrame_baseSet, contMDiffOn_iff_of_mem_maximalAtlas', contMDiffOn_continuousLinearMapCoordChange, contMDiffOn_extChartAt_symm, IsLocalFrameOn.contMDiffOn, IsLocalDiffeomorphAt.contmdiffOn_localInverse, IsLocalDiffeomorphOn.contMDiffOn, contMDiffOn_iff_of_subset_source', isLocalStructomorphOn_contDiffGroupoid_iff, contMDiffWithinAt_iff_contMDiffOn_nhds, contMDiffOn_iUnion_iff_of_isOpen, contMDiffOn_of_mem_contDiffGroupoid, contMDiffOn_symm_coordChangeL, Trivialization.contMDiffOn_section_baseSet_iff, Diffeomorph.contMDiffOn_diffeomorph_comp_iff, Bundle.contMDiffOn_proj, contMDiffOn_fst, contMDiffOn_prod_iff, contMDiffOn_iff, contMDiffOn_iff_source_of_mem_maximalAtlas, ContMDiffWithinAt.contMDiffOn', ContMDiffVectorBundle.contMDiffOn_coordChangeL, VectorBundleCore.IsContMDiff.contMDiffOn_coordChange, contMDiffOn_univ, contMDiffOn_iff_of_mem_maximalAtlas, contMDiffOn_iff_of_subset_source, contMDiffOn_of_mem_maximalAtlas, contMDiffOn_comp_projIcc_iff, contMDiffOn_const, PartialDiffeomorph.contMDiffOn_invFun, contMDiffOn_extend_symm, VectorPrebundle.contMDiffOn_contMDiffCoordChange, Trivialization.contMDiffOn_symm, Trivialization.contMDiffOn_iff, isLocalStructomorphOn_contDiffGroupoid_iff_aux, VectorPrebundle.IsContMDiff.exists_contMDiffCoordChange, ContinuousLinearMap.contMDiffOn, contMDiffOn_coordChangeL, contMDiffOn_model_symm, ContinuousLinearEquiv.contMDiffOn_transContinuousLinearEquiv_left, ContMDiffWithinAt.contMDiffOn, contMDiffOn_one, contMDiffOn_empty, contMDiffOn_union_iff_of_isOpen, contMDiffOn_iff_target, contMDiffOn_symm_of_mem_maximalAtlas, contMDiffOn_vectorSpace_iff_contDiffOn, Manifold.exists_lt_of_riemannianEDist_lt, contMDiffOn_zero_iff, contMDiffOn_snd, contMDiffOn_prod_module_iff, Trivialization.contMDiffOn, contMDiffOn_congr, contMDiffOn_section_of_mem_baseSet₀, contMDiffOn_id, contMDiffOn_infty, ContinuousLinearEquiv.contMDiffOn_transContinuousLinearEquiv_right, contMDiffOn_projIcc, contMDiffOn_section_of_mem_baseSet
ContMDiffWithinAt 📖	MathDef	61 math math: contMDiffWithinAt_insert_self, Diffeomorph.contMDiffWithinAt, contMDiffWithinAt_iff_target, contMDiffWithinAt_congr_set', ContDiffWithinAt.contMDiffWithinAt, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt, contMDiffWithinAt_congr_of_mem, contMDiffWithinAt_iff_contMDiffWithinAt_nhdsWithin, contMDiffAt_iff_source, ContMDiffAt.contMDiffWithinAt, contMDiffWithinAt_inter', Bundle.contMDiffWithinAt_zeroSection, contMDiffWithinAt_iff_image, contMDiffWithinAt_snd, contMDiffWithinAt_prod_iff, contMDiffWithinAt_congr_set, contMDiffWithinAt_prod_module_iff, contMDiffWithinAt_pi_space, contMDiffAt_iff_source_of_mem_source, contMDiffWithinAt_const, contMDiffWithinAt_zero, contMDiffWithinAt_iff_of_mem_source', contMDiffWithinAt_extChartAt_symm_range_self, contMDiffWithinAt_iff_target_of_mem_source, Bundle.contMDiffWithinAt_totalSpace, contMDiffWithinAt_iff_source_of_mem_maximalAtlas, contMDiffWithinAt_one, contMDiffWithinAt_iff_contMDiffOn_nhds, contMDiffWithinAt_iff_le_ne_infty, contMDiffWithinAt_iff, contMDiffWithinAt_of_subsingleton, Bundle.contMDiffWithinAt_proj, contMDiffWithinAt_id, ContinuousLinearEquiv.contMDiffWithinAt_transContinuousLinearEquiv_right, contMDiffWithinAt_comp_projIcc_iff, contMDiffWithinAt_fst, contMDiffWithinAt_iff', Diffeomorph.contMDiffWithinAt_comp_diffeomorph_iff, contMDiffWithinAt_extChartAt_symm_target_self, contMDiffWithinAt_inter, contMDiffWithinAt_iff_contDiffWithinAt, ContinuousLinearEquiv.contMDiffWithinAt_transContinuousLinearEquiv_left, contMDiffWithinAt_extChartAt_symm_target, Trivialization.contMDiffWithinAt_iff, contMDiffWithinAt_iff_source, contMDiffWithinAt_iff_source_of_mem_source, contMDiffWithinAt_iff_of_mem_maximalAtlas, contMDiffWithinAt_univ, contMDiffWithinAt_infty, contMDiffWithinAt_extChartAt_symm_range, Diffeomorph.contMDiffWithinAt_diffeomorph_comp_iff, ContinuousLinearMap.contMDiffWithinAt, Bundle.contMDiffWithinAt_section, contMDiffWithinAt_of_notMem_mulTSupport, contMDiffWithinAt_of_notMem, contMDiffWithinAt_iff_nat, contMDiffWithinAt_congr, Filter.EventuallyEq.contMDiffWithinAt_iff, contMDiffWithinAt_hom_bundle, contMDiffWithinAt_iff_of_mem_source, Trivialization.contMDiffWithinAt_section

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffWithinAtProp_id 📖	mathematical	—	ContDiffWithinAtProp Set.univ	—	Set.univ_inter ContDiffAt.contDiffWithinAt ContDiff.contDiffAt contDiff_id ContDiffWithinAt.congr ModelWithCorners.right_inv ModelWithCorners.left_inv
contDiffWithinAtProp_mono_of_mem_nhdsWithin 📖	—	Set Filter Filter.instMembership nhdsWithin ContDiffWithinAtProp	—	—	ContDiffWithinAt.mono_of_mem_nhdsWithin Filter.inter_mem Filter.mem_map ModelWithCorners.image_eq ModelWithCorners.symm_map_nhdsWithin_image Filter.mem_of_superset self_mem_nhdsWithin Set.inter_subset_right
contDiffWithinAtProp_self 📖	mathematical	—	ContDiffWithinAtProp UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf ContDiffWithinAt	—	contDiffWithinAtProp_self_source
contDiffWithinAtProp_self_source 📖	mathematical	—	ContDiffWithinAtProp UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf ContDiffWithinAt ModelWithCorners.toFun'	—	Set.range_id Set.inter_univ CompTriple.comp_eq CompTriple.instComp_id CompTriple.instIsIdId
contDiffWithinAtProp_self_target 📖	mathematical	—	ContDiffWithinAtProp UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf ContDiffWithinAt PartialEquiv.toFun ModelWithCorners.symm Set Set.instInter Set.preimage Set.range ModelWithCorners.toFun'	—	—
contDiffWithinAt_localInvariantProp 📖	mathematical	—	StructureGroupoid.LocalInvariantProp contDiffGroupoid ContDiffWithinAtProp	—	contDiffWithinAt_localInvariantProp_of_le le_rfl
contDiffWithinAt_localInvariantProp_of_le 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat	StructureGroupoid.LocalInvariantProp contDiffGroupoid ContDiffWithinAtProp	—	Set.inter_right_comm ContDiffWithinAtProp.eq_1 contDiffWithinAt_inter ModelWithCorners.left_inv IsOpen.mem_nhds ContinuousAt.preimage_mem_nhds Continuous.continuousAt ModelWithCorners.continuous_symm OpenPartialHomeomorph.left_inv ContDiffOn.contDiffWithinAt mem_groupoid_of_pregroupoid ContDiffWithinAt.mono_of_mem_nhdsWithin ContDiffWithinAt.comp_inter ContDiffWithinAt.of_le mem_nhdsWithin IsOpen.preimage OpenPartialHomeomorph.open_target OpenPartialHomeomorph.mapsTo ContDiffWithinAt.congr ContDiffWithinAt.comp
contMDiffAt_iff 📖	mathematical	—	ContMDiffAt ContinuousAt ContDiffWithinAt PartialEquiv.toFun extChartAt PartialEquiv.symm Set.range ModelWithCorners.toFun'	—	ChartedSpace.liftPropAt_iff ContDiffWithinAtProp.eq_1 Set.preimage_univ Set.univ_inter
contMDiffAt_iff_contMDiffAt_nhds 📖	mathematical	—	ContMDiffAt Filter.Eventually nhds	—	contMDiffAt_iff_contMDiffOn_nhds Filter.Eventually.mono eventually_mem_nhds_iff ContMDiffWithinAt.contMDiffAt mem_of_mem_nhds Filter.Eventually.self_of_nhds
contMDiffAt_iff_contMDiffOn_nhds 📖	mathematical	—	ContMDiffAt Set Filter Filter.instMembership nhds ContMDiffOn	—	contMDiffWithinAt_iff_contMDiffOn_nhds Set.insert_eq_of_mem nhdsWithin_univ
contMDiffAt_iff_le_ne_infty 📖	mathematical	—	ContMDiffAt	—	contMDiffWithinAt_iff_le_ne_infty
contMDiffAt_iff_nat 📖	mathematical	—	ContMDiffAt WithTop.some ENat WithTop AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	—
contMDiffAt_iff_of_mem_source 📖	mathematical	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv chartAt	ContMDiffAt ContinuousAt ContDiffWithinAt PartialEquiv.toFun extChartAt PartialEquiv.symm Set.range ModelWithCorners.toFun'	—	contMDiffWithinAt_iff_of_mem_source continuousWithinAt_univ Set.preimage_univ Set.univ_inter
contMDiffAt_iff_source 📖	mathematical	—	ContMDiffAt ContMDiffWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun PartialEquiv.symm extChartAt Set.range ModelWithCorners.toFun'	—	contMDiffWithinAt_univ contMDiffWithinAt_iff_source Set.univ_inter
contMDiffAt_iff_source_of_mem_source 📖	mathematical	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv chartAt	ContMDiffAt ContMDiffWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun PartialEquiv.symm extChartAt Set.range ModelWithCorners.toFun'	—	contMDiffWithinAt_iff_source_of_mem_source Set.univ_inter
contMDiffAt_iff_target 📖	mathematical	—	ContMDiffAt ContinuousAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun extChartAt	—	ContMDiffAt.eq_1 contMDiffWithinAt_iff_target continuousWithinAt_univ
contMDiffAt_iff_target_of_mem_source 📖	mathematical	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv chartAt	ContMDiffAt ContinuousAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun extChartAt	—	ContMDiffAt.eq_1 contMDiffWithinAt_iff_target_of_mem_source continuousWithinAt_univ
contMDiffAt_infty 📖	mathematical	—	ContMDiffAt WithTop.some ENat Top.top instTopENat WithTop AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	contMDiffWithinAt_infty
contMDiffOn_congr 📖	mathematical	—	ContMDiffOn	—	StructureGroupoid.LocalInvariantProp.liftPropOn_congr_iff contDiffWithinAt_localInvariantProp
contMDiffOn_empty 📖	mathematical	—	ContMDiffOn Set Set.instEmptyCollection	—	—
contMDiffOn_iff 📖	mathematical	—	ContMDiffOn ContinuousOn ContDiffOn PartialEquiv.toFun extChartAt PartialEquiv.symm Set Set.instInter PartialEquiv.target Set.preimage PartialEquiv.source	—	ChartedSpace.LiftPropWithinAt.continuousWithinAt ModelWithCorners.target_eq ModelWithCorners.source_eq Set.inter_univ OpenPartialHomeomorph.right_inv ModelWithCorners.right_inv ContDiffWithinAt.mono contMDiffWithinAt_iff_of_mem_source StructureGroupoid.LocalInvariantProp.liftPropWithinAt_iff contDiffWithinAt_localInvariantProp Set.ext ModelWithCorners.left_inv OpenPartialHomeomorph.left_inv
contMDiffOn_iff_of_mem_maximalAtlas 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership IsManifold.maximalAtlas Set.instHasSubset PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv Set.MapsTo	ContMDiffOn ContinuousOn ContDiffOn PartialEquiv.toFun OpenPartialHomeomorph.extend PartialEquiv.symm Set.image	—	contMDiffWithinAt_iff_image
contMDiffOn_iff_of_mem_maximalAtlas' 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership IsManifold.maximalAtlas Set.instHasSubset PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv Set.MapsTo	ContMDiffOn ContDiffOn PartialEquiv.toFun OpenPartialHomeomorph.extend PartialEquiv.symm Set.image	—	contMDiffOn_iff_of_mem_maximalAtlas OpenPartialHomeomorph.continuousOn_writtenInExtend_iff ContDiffOn.continuousOn
contMDiffOn_iff_of_subset_source 📖	mathematical	Set Set.instHasSubset PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv chartAt Set.MapsTo	ContMDiffOn ContinuousOn ContDiffOn PartialEquiv.toFun extChartAt PartialEquiv.symm Set.image	—	contMDiffOn_iff_of_mem_maximalAtlas IsManifold.chart_mem_maximalAtlas
contMDiffOn_iff_of_subset_source' 📖	mathematical	Set Set.instHasSubset PartialEquiv.source extChartAt Set.MapsTo	ContMDiffOn ContDiffOn PartialEquiv.toFun PartialEquiv.symm Set.image	—	contMDiffOn_iff_of_mem_maximalAtlas' IsManifold.chart_mem_maximalAtlas extChartAt_source
contMDiffOn_iff_source_of_mem_maximalAtlas 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership IsManifold.maximalAtlas Set.instHasSubset PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	ContMDiffOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun PartialEquiv.symm OpenPartialHomeomorph.extend Set.image	—	contMDiffWithinAt_iff_source_of_mem_maximalAtlas contMDiffWithinAt_congr_set OpenPartialHomeomorph.extend_symm_preimage_inter_range_eventuallyEq
contMDiffOn_iff_target 📖	mathematical	—	ContMDiffOn ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun extChartAt Set Set.instInter Set.preimage PartialEquiv.source	—	IsManifold.instOfTopWithTopENat instIsManifoldModelSpace PartialEquiv.refl_trans ModelWithCorners.source_eq Set.inter_univ Continuous.continuousOn ModelWithCorners.continuous ContinuousOn.comp_inter OpenPartialHomeomorph.continuousOn_toFun
contMDiffOn_infty 📖	mathematical	—	ContMDiffOn WithTop.some ENat Top.top instTopENat WithTop AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	ContMDiffOn.of_le le_top contMDiffWithinAt_infty
contMDiffOn_of_locally_contMDiffOn 📖	—	IsOpen Set Set.instMembership ContMDiffOn Set.instInter	—	—	StructureGroupoid.LocalInvariantProp.liftPropOn_of_locally_liftPropOn contDiffWithinAt_localInvariantProp
contMDiffOn_univ 📖	mathematical	—	ContMDiffOn Set.univ ContMDiff	—	—
contMDiffOn_zero_iff 📖	mathematical	—	ContMDiffOn WithTop ENat WithTop.zero instZeroENat ContinuousOn	—	contMDiffOn_iff IsManifold.instOfNatWithTopENat contDiffOn_zero ContinuousOn.comp continuousOn_extChartAt ContinuousOn.mono continuousOn_extChartAt_symm Set.inter_subset_left
contMDiffWithinAt_congr 📖	mathematical	—	ContMDiffWithinAt	—	StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff contDiffWithinAt_localInvariantProp
contMDiffWithinAt_congr_of_mem 📖	mathematical	Set Set.instMembership	ContMDiffWithinAt	—	StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff_of_mem contDiffWithinAt_localInvariantProp
contMDiffWithinAt_congr_set 📖	mathematical	Filter.EventuallyEq nhds	ContMDiffWithinAt	—	StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_set contDiffWithinAt_localInvariantProp
contMDiffWithinAt_congr_set' 📖	mathematical	Filter.EventuallyEq nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	ContMDiffWithinAt	—	ModelWithCorners.t1Space contMDiffWithinAt_insert_self contMDiffWithinAt_congr_set eventuallyEq_insert
contMDiffWithinAt_iff 📖	mathematical	—	ContMDiffWithinAt ContinuousWithinAt ContDiffWithinAt PartialEquiv.toFun extChartAt PartialEquiv.symm Set Set.instInter Set.preimage Set.range ModelWithCorners.toFun'	—	—
contMDiffWithinAt_iff' 📖	mathematical	—	ContMDiffWithinAt ContinuousWithinAt ContDiffWithinAt PartialEquiv.toFun extChartAt PartialEquiv.symm Set Set.instInter PartialEquiv.target Set.preimage PartialEquiv.source	—	contDiffWithinAt_congr_set ContinuousWithinAt.extChartAt_symm_preimage_inter_range_eventuallyEq
contMDiffWithinAt_iff_contMDiffOn_nhds 📖	mathematical	—	ContMDiffWithinAt Set Filter Filter.instMembership nhdsWithin Set.instInsert ContMDiffOn	—	Set.insert_eq_of_mem ContDiffWithinAt.contDiffOn le_rfl instIsEmptyFalse contMDiffWithinAt_iff' PartialEquiv.map_source mem_extChartAt_source extChartAt_to_inv map_extChartAt_symm_nhdsWithin ContinuousWithinAt.nhdsWithin_extChartAt_symm_preimage_inter_range ChartedSpace.LiftPropWithinAt.continuousWithinAt Filter.image_mem_map Set.image_subset_iff PartialEquiv.map_target contMDiffOn_iff_of_subset_source' PartialEquiv.image_symm_image_of_subset_target HasSubset.Subset.trans Set.instIsTransSubset Set.inter_subset_left ContMDiffWithinAt.mono_of_mem_nhdsWithin mem_of_mem_nhdsWithin contMDiffWithinAt_insert_self Set.mem_insert Set.insert_idem
contMDiffWithinAt_iff_contMDiffWithinAt_nhdsWithin 📖	mathematical	—	ContMDiffWithinAt Filter.Eventually nhdsWithin Set Set.instInsert	—	contMDiffWithinAt_iff_contMDiffOn_nhds Filter.mp_mem eventually_mem_nhdsWithin_iff Filter.univ_mem' ContMDiffWithinAt.mono_of_mem_nhdsWithin nhdsWithin_mono Set.subset_insert mem_of_mem_nhdsWithin Set.mem_insert
contMDiffWithinAt_iff_image 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership IsManifold.maximalAtlas Set.instHasSubset PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	ContMDiffWithinAt ContinuousWithinAt ContDiffWithinAt PartialEquiv.toFun OpenPartialHomeomorph.extend PartialEquiv.symm Set.image	—	contMDiffWithinAt_iff_of_mem_maximalAtlas contDiffWithinAt_congr_set OpenPartialHomeomorph.extend_symm_preimage_inter_range_eventuallyEq
contMDiffWithinAt_iff_le_ne_infty 📖	mathematical	—	ContMDiffWithinAt	—	ContMDiffWithinAt.of_le le_rfl contMDiffWithinAt_iff_nat
contMDiffWithinAt_iff_nat 📖	mathematical	—	ContMDiffWithinAt WithTop.some ENat WithTop AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	ContMDiffWithinAt.of_le contMDiffWithinAt_infty le_top le_rfl
contMDiffWithinAt_iff_of_mem_maximalAtlas 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership IsManifold.maximalAtlas PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	ContMDiffWithinAt ContinuousWithinAt ContDiffWithinAt PartialEquiv.toFun OpenPartialHomeomorph.extend PartialEquiv.symm Set.instInter Set.preimage Set.range ModelWithCorners.toFun'	—	StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart contDiffWithinAt_localInvariantProp IsManifold.toHasGroupoid
contMDiffWithinAt_iff_of_mem_source 📖	mathematical	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv chartAt	ContMDiffWithinAt ContinuousWithinAt ContDiffWithinAt PartialEquiv.toFun extChartAt PartialEquiv.symm Set.instInter Set.preimage Set.range ModelWithCorners.toFun'	—	contMDiffWithinAt_iff_of_mem_maximalAtlas IsManifold.chart_mem_maximalAtlas
contMDiffWithinAt_iff_of_mem_source' 📖	mathematical	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv chartAt	ContMDiffWithinAt ContinuousWithinAt ContDiffWithinAt PartialEquiv.toFun extChartAt PartialEquiv.symm Set.instInter PartialEquiv.target Set.preimage	—	contMDiffWithinAt_iff_of_mem_source contDiffWithinAt_congr_set nhdsWithin_eq_iff_eventuallyEq PartialEquiv.image_source_inter_eq' map_extChartAt_nhdsWithin_eq_image' extChartAt_source map_extChartAt_nhdsWithin' Set.inter_comm nhdsWithin_inter_of_mem extChartAt_source_mem_nhds'
contMDiffWithinAt_iff_source 📖	mathematical	—	ContMDiffWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun PartialEquiv.symm extChartAt Set Set.instInter Set.preimage Set.range ModelWithCorners.toFun'	—	ContinuousWithinAt.comp_of_eq ContinuousAt.continuousWithinAt continuousAt_extChartAt_symm Set.MapsTo.mono_left Set.mapsTo_preimage Set.inter_subset_left extChartAt_to_inv continuousWithinAt_inter extChartAt_source_mem_nhds ContinuousWithinAt.comp continuousAt_extChartAt OpenPartialHomeomorph.left_inv ModelWithCorners.source_eq Set.inter_univ ModelWithCorners.left_inv ContinuousWithinAt.congr Set.range_id
contMDiffWithinAt_iff_source_of_mem_maximalAtlas 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership IsManifold.maximalAtlas PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	ContMDiffWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun PartialEquiv.symm OpenPartialHomeomorph.extend Set.instInter Set.preimage Set.range ModelWithCorners.toFun'	—	StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_source contDiffWithinAt_localInvariantProp IsManifold.toHasGroupoid OpenPartialHomeomorph.extend_symm_continuousWithinAt_comp_right_iff OpenPartialHomeomorph.left_inv PartialEquiv.left_inv OpenPartialHomeomorph.extend_source
contMDiffWithinAt_iff_source_of_mem_source 📖	mathematical	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv chartAt	ContMDiffWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun PartialEquiv.symm extChartAt Set.instInter Set.preimage Set.range ModelWithCorners.toFun'	—	contMDiffWithinAt_iff_source_of_mem_maximalAtlas IsManifold.chart_mem_maximalAtlas
contMDiffWithinAt_iff_target 📖	mathematical	—	ContMDiffWithinAt ContinuousWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun extChartAt	—	ContinuousAt.comp_continuousWithinAt continuousAt_extChartAt
contMDiffWithinAt_iff_target_of_mem_source 📖	mathematical	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv chartAt	ContMDiffWithinAt ContinuousWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun extChartAt	—	StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target contDiffWithinAt_localInvariantProp IsManifold.toHasGroupoid IsManifold.chart_mem_maximalAtlas ContinuousAt.comp_continuousWithinAt OpenPartialHomeomorph.continuousAt continuousAt_extChartAt' extChartAt_source
contMDiffWithinAt_infty 📖	mathematical	—	ContMDiffWithinAt WithTop.some ENat Top.top instTopENat WithTop AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	ChartedSpace.LiftPropWithinAt.continuousWithinAt contDiffWithinAt_infty ChartedSpace.LiftPropWithinAt.prop
contMDiffWithinAt_insert_self 📖	mathematical	—	ContMDiffWithinAt Set Set.instInsert	—	Iff.and contDiffWithinAt_congr_set nhdsWithin_insert Filter.map_sup contDiffWithinAt_insert_self
contMDiffWithinAt_inter 📖	mathematical	Set Filter Filter.instMembership nhds	ContMDiffWithinAt Set.instInter	—	StructureGroupoid.LocalInvariantProp.liftPropWithinAt_inter contDiffWithinAt_localInvariantProp
contMDiffWithinAt_inter' 📖	mathematical	Set Filter Filter.instMembership nhdsWithin	ContMDiffWithinAt Set.instInter	—	StructureGroupoid.LocalInvariantProp.liftPropWithinAt_inter' contDiffWithinAt_localInvariantProp
contMDiffWithinAt_univ 📖	mathematical	—	ContMDiffWithinAt Set.univ ContMDiffAt	—	—
contMDiff_congr 📖	mathematical	—	ContMDiff	—	contMDiffOn_congr
contMDiff_iff 📖	mathematical	—	ContMDiff Continuous ContDiffOn PartialEquiv.toFun extChartAt PartialEquiv.symm Set Set.instInter PartialEquiv.target Set.preimage PartialEquiv.source	—	ModelWithCorners.target_eq ModelWithCorners.source_eq Set.inter_univ Set.univ_inter
contMDiff_iff_target 📖	mathematical	—	ContMDiff Continuous ContMDiffOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun extChartAt Set.preimage PartialEquiv.source	—	contMDiffOn_univ contMDiffOn_iff_target ModelWithCorners.source_eq Set.inter_univ Set.univ_inter
contMDiff_infty 📖	mathematical	—	ContMDiff WithTop.some ENat Top.top instTopENat WithTop AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	ContMDiff.of_le le_top contMDiffWithinAt_infty
contMDiff_of_locally_contMDiffOn 📖	mathematical	IsOpen Set Set.instMembership ContMDiffOn	ContMDiff	—	StructureGroupoid.LocalInvariantProp.liftProp_of_locally_liftPropOn contDiffWithinAt_localInvariantProp
contMDiff_zero_iff 📖	mathematical	—	ContMDiff WithTop ENat WithTop.zero instZeroENat Continuous	—	contMDiffOn_univ continuousOn_univ contMDiffOn_zero_iff

---

← Back to Index