WhitneyEmbedding

📁 Source: Mathlib/Geometry/Manifold/WhitneyEmbedding.lean

Statistics

Metric	Count
Definitions embeddingPiTangent	1
Theorems comp_embeddingPiTangent_mfderiv, embeddingPiTangent_coe, embeddingPiTangent_injOn, embeddingPiTangent_injective, embeddingPiTangent_injective_mfderiv, embeddingPiTangent_ker_mfderiv, exists_immersion_euclidean, exists_embedding_euclidean_of_compact	8
Total	9

SmoothBumpCovering

Definitions

Name	Category	Theorems
embeddingPiTangent 📖	CompOp	6 math math: embeddingPiTangent_injective_mfderiv, embeddingPiTangent_ker_mfderiv, embeddingPiTangent_injOn, comp_embeddingPiTangent_mfderiv, embeddingPiTangent_injective, embeddingPiTangent_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_embeddingPiTangent_mfderiv 📖	mathematical	Set Set.instMembership	ContinuousLinearMap.comp Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.semiring RingHom.id Semiring.toNonAssocSemiring TangentSpace instTopologicalSpaceTangentSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.topologicalSpace instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.pseudoMetricSpace Pi.addCommMonoid Prod.instAddCommMonoid Real.instAddCommMonoid instModuleTangentSpace Pi.module Module Prod.instModule NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal RingHomCompTriple.ids ContinuousLinearMap.fst ContinuousLinearMap.proj ind mfderiv Pi.normedAddCommGroup Prod.normedAddCommGroup Real.normedAddCommGroup Pi.normedSpace Prod.seminormedAddCommGroup Prod.normedSpace modelWithCornersSelf chartedSpaceSelf DFunLike.coe ContMDiffMap WithTop.some ENat Top.top instTopENat ContMDiffMap.instFunLike embeddingPiTangent OpenPartialHomeomorph.toFun' chartAt c	—	RingHomCompTriple.ids HasMFDerivAt.comp ContinuousLinearMap.hasMFDerivAt MDifferentiableAt.hasMFDerivAt ContMDiff.mdifferentiableAt ContMDiffMap.contMDiff hasMFDerivAt_unique HasMFDerivAt.congr_of_eventuallyEq hasMFDerivAt_extChartAt IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfSomeENatTopOfLEInfty Nat.instAtLeastTwoHAddOfNat IsManifold.instLEInftyOfNatWithTopENat mem_chartAt_ind_source Filter.Eventually.mono eventuallyEq_one Pi.one_apply one_smul
embeddingPiTangent_coe 📖	mathematical	—	DFunLike.coe ContMDiffMap Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Pi.normedAddCommGroup Prod.normedAddCommGroup Real.normedAddCommGroup Pi.normedSpace NontriviallyNormedField.toNormedField Prod.seminormedAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Prod.normedSpace InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf Pi.topologicalSpace instTopologicalSpaceProd Real.pseudoMetricSpace chartedSpaceSelf WithTop.some ENat Top.top instTopENat ContMDiffMap.instFunLike embeddingPiTangent SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField SmoothBumpFunction.toFun c toFun PartialEquiv.toFun extChartAt	—	—
embeddingPiTangent_injOn 📖	mathematical	—	Set.InjOn DFunLike.coe ContMDiffMap Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Pi.normedAddCommGroup Prod.normedAddCommGroup Real.normedAddCommGroup Pi.normedSpace NontriviallyNormedField.toNormedField Prod.seminormedAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Prod.normedSpace InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf Pi.topologicalSpace instTopologicalSpaceProd Real.pseudoMetricSpace chartedSpaceSelf WithTop.some ENat Top.top instTopENat ContMDiffMap.instFunLike embeddingPiTangent	—	mem_extChartAt_source_of_eq_one apply_ind PartialEquiv.injOn mem_extChartAt_ind_source one_smul
embeddingPiTangent_injective 📖	mathematical	—	DFunLike.coe ContMDiffMap Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Pi.normedAddCommGroup Prod.normedAddCommGroup Real.normedAddCommGroup Pi.normedSpace NontriviallyNormedField.toNormedField Prod.seminormedAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Prod.normedSpace InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf Pi.topologicalSpace instTopologicalSpaceProd Real.pseudoMetricSpace chartedSpaceSelf WithTop.some ENat Top.top instTopENat ContMDiffMap.instFunLike embeddingPiTangent Set.univ	—	Set.injOn_univ embeddingPiTangent_injOn
embeddingPiTangent_injective_mfderiv 📖	mathematical	Set Set.instMembership	TangentSpace Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Pi.normedAddCommGroup Prod.normedAddCommGroup Real.normedAddCommGroup Pi.normedSpace NontriviallyNormedField.toNormedField Prod.seminormedAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Prod.normedSpace InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf Pi.topologicalSpace instTopologicalSpaceProd Real.pseudoMetricSpace chartedSpaceSelf DFunLike.coe ContMDiffMap WithTop.some ENat Top.top instTopENat ContMDiffMap.instFunLike embeddingPiTangent ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceTangentSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace ContinuousLinearMap.funLike mfderiv	—	LinearMap.ker_eq_bot embeddingPiTangent_ker_mfderiv
embeddingPiTangent_ker_mfderiv 📖	mathematical	Set Set.instMembership	LinearMap.ker Real TangentSpace DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Pi.normedAddCommGroup Prod.normedAddCommGroup Real.normedAddCommGroup Pi.normedSpace NontriviallyNormedField.toNormedField Prod.seminormedAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Prod.normedSpace InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf Pi.topologicalSpace instTopologicalSpaceProd Real.pseudoMetricSpace chartedSpaceSelf DFunLike.coe ContMDiffMap WithTop.some ENat Top.top instTopENat ContMDiffMap.instFunLike embeddingPiTangent DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid instTopologicalSpaceTangentSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.toLinearMap mfderiv Bot.bot Submodule Submodule.instBot	—	bot_unique OpenPartialHomeomorph.MDifferentiable.ker_mfderiv_eq_bot mdifferentiable_chart IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfSomeENatTopOfLEInfty Nat.instAtLeastTwoHAddOfNat IsManifold.instLEInftyOfNatWithTopENat mem_chartAt_ind_source RingHomCompTriple.ids comp_embeddingPiTangent_mfderiv LinearMap.ker_le_ker_comp
exists_immersion_euclidean 📖	mathematical	—	ContMDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField EuclideanSpace PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal Fin.fintype Real.normedAddCommGroup PiLp.normedSpace NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf PiLp.topologicalSpace Real.pseudoMetricSpace chartedSpaceSelf WithTop.some ENat Top.top instTopENat TangentSpace DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceTangentSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace ContinuousLinearMap.funLike mfderiv	—	nonempty_fintype fact_one_le_two_ennreal RingHomInvPair.ids Pi.topologicalAddGroup Prod.instIsTopologicalAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup instIsTopologicalAddGroupReal instContinuousSMulForall Prod.continuousSMul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal PiLp.instIsBoundedSMul Real.isBoundedSMul Real.instCompleteSpace Pi.t2Space Prod.t2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace IsNoetherian.iff_fg isNoetherian_pi' Module.instFiniteDimensionalOfIsReflexive Prod.instModuleIsReflexive Module.instIsReflexiveOfFiniteOfProjective Module.Projective.of_free Module.Free.of_divisionRing FiniteDimensional.rclike_to_real Module.Free.self WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype finrank_euclideanSpace_fin ContMDiff.comp Diffeomorph.contMDiff ContMDiffMap.contMDiff ContinuousLinearEquiv.injective embeddingPiTangent_injective RingHomCompTriple.ids mfderiv_comp DifferentiableAt.mdifferentiableAt ContinuousLinearEquiv.differentiableAt ContMDiff.mdifferentiableAt ContinuousLinearEquiv.mfderiv_eq embeddingPiTangent_injective_mfderiv

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_embedding_euclidean_of_compact 📖	mathematical	—	ContMDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField EuclideanSpace PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal Fin.fintype Real.normedAddCommGroup PiLp.normedSpace NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf PiLp.topologicalSpace Real.pseudoMetricSpace chartedSpaceSelf WithTop.some ENat Top.top instTopENat Topology.IsClosedEmbedding TangentSpace DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceTangentSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace ContinuousLinearMap.funLike mfderiv	—	fact_one_le_two_ennreal SmoothBumpCovering.exists_isSubordinate CompactSpace.sigmaCompact isClosed_univ Filter.univ_mem SmoothBumpCovering.exists_immersion_euclidean Finite.of_fintype Continuous.isClosedEmbedding TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ContMDiff.continuous

---

← Back to Index