UniqueDifferential

📁 Source: Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean

Statistics

Metric	Count
Definitions	0
Theorems mdifferentiable, bundle_preimage, image_denseRange, image_denseRange', uniqueDiffOn_inter_preimage, uniqueDiffOn_target_inter, uniqueDiffWithinAt_range_inter, uniqueMDiffOn_preimage, uniqueMDiffOn_target_inter, bundle_preimage, bundle_preimage', image_denseRange, preimage_PartialHomeomorph, preimage_openPartialHomeomorph	14
Total	14

Trivialization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mdifferentiable 📖	mathematical	—	OpenPartialHomeomorph.MDifferentiable Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace FiberBundle.chartedSpace instTopologicalSpaceProd prodChartedSpace chartedSpaceSelf toOpenPartialHomeomorph Bundle.TotalSpace.proj	—	ContMDiffOn.mdifferentiableOn contMDiffOn one_ne_zero NeZero.charZero_one WithTop.charZero contMDiffOn_symm

UniqueMDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bundle_preimage 📖	mathematical	UniqueMDiffOn	Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace FiberBundle.chartedSpace Set.preimage Bundle.TotalSpace.proj	—	UniqueMDiffWithinAt.bundle_preimage
image_denseRange 📖	mathematical	UniqueMDiffOn MDifferentiableOn DenseRange TangentSpace instTopologicalSpaceTangentSpace DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace ContinuousLinearMap.funLike mfderivWithin	Set.image	—	image_denseRange' MDifferentiableWithinAt.hasMFDerivWithinAt
image_denseRange' 📖	mathematical	UniqueMDiffOn HasMFDerivWithinAt DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike	Set.image	—	Set.forall_mem_image UniqueMDiffWithinAt.image_denseRange
uniqueDiffOn_inter_preimage 📖	mathematical	UniqueMDiffOn ContinuousOn	UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instInter PartialEquiv.target extChartAt Set.preimage PartialEquiv.toFun PartialEquiv.symm PartialEquiv.source	—	uniqueDiffOn_target_inter UniqueMDiffWithinAt.inter' ContinuousWithinAt.preimage_mem_nhdsWithin IsOpen.mem_nhds isOpen_extChartAt_source
uniqueDiffOn_target_inter 📖	mathematical	UniqueMDiffOn	UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instInter PartialEquiv.target extChartAt Set.preimage PartialEquiv.toFun PartialEquiv.symm	—	uniqueDiffOn uniqueMDiffOn_target_inter
uniqueDiffWithinAt_range_inter 📖	mathematical	UniqueMDiffOn Set Set.instMembership Set.instInter PartialEquiv.target extChartAt Set.preimage PartialEquiv.toFun PartialEquiv.symm	UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set.range ModelWithCorners.toFun'	—	UniqueDiffWithinAt.mono uniqueDiffOn_target_inter Set.inter_subset_inter_left extChartAt_target_subset_range
uniqueMDiffOn_preimage 📖	mathematical	UniqueMDiffOn OpenPartialHomeomorph.MDifferentiable	Set Set.instInter PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv Set.preimage OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm	—	UniqueMDiffWithinAt.preimage_openPartialHomeomorph OpenPartialHomeomorph.map_target OpenPartialHomeomorph.right_inv
uniqueMDiffOn_target_inter 📖	mathematical	UniqueMDiffOn	UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf Set Set.instInter PartialEquiv.target extChartAt Set.preimage PartialEquiv.toFun PartialEquiv.symm	—	PartialEquiv.image_source_inter_eq' Set.inter_comm extChartAt_source image_denseRange' inter OpenPartialHomeomorph.open_source hasMFDerivWithinAt_extChartAt Function.Surjective.denseRange OpenPartialHomeomorph.MDifferentiable.mfderiv_surjective mdifferentiable_chart

UniqueMDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bundle_preimage 📖	mathematical	UniqueMDiffWithinAt Bundle.TotalSpace.proj	Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace FiberBundle.chartedSpace Set.preimage	—	inter IsOpen.mem_nhds Trivialization.open_baseSet FiberBundle.mem_baseSet_trivializationAt' Set.inter_subset_right mono
bundle_preimage' 📖	mathematical	UniqueMDiffWithinAt	Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace FiberBundle.chartedSpace Set.preimage Bundle.TotalSpace.proj	—	bundle_preimage
image_denseRange 📖	mathematical	UniqueMDiffWithinAt HasMFDerivWithinAt DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike	Set.image	—	inter' extChartAt_source_mem_nhds UniqueDiffWithinAt.congr_pt UniqueDiffWithinAt.mono HasFDerivWithinAt.uniqueDiffWithinAt HasFDerivWithinAt.mono ModelWithCorners.source_eq Set.inter_univ PartialEquiv.left_inv Set.mem_range_self ModelWithCorners.left_inv OpenPartialHomeomorph.left_inv
preimage_PartialHomeomorph 📖	mathematical	UniqueMDiffWithinAt OpenPartialHomeomorph.MDifferentiable Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	Set.instInter PartialEquiv.target Set.preimage OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm	—	preimage_openPartialHomeomorph
preimage_openPartialHomeomorph 📖	mathematical	UniqueMDiffWithinAt OpenPartialHomeomorph.MDifferentiable Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	Set.instInter PartialEquiv.target Set.preimage OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm	—	OpenPartialHomeomorph.image_source_inter_eq' Set.inter_comm image_denseRange inter IsOpen.mem_nhds OpenPartialHomeomorph.open_source HasMFDerivAt.hasMFDerivWithinAt MDifferentiableAt.hasMFDerivAt OpenPartialHomeomorph.MDifferentiable.mdifferentiableAt Function.Surjective.denseRange OpenPartialHomeomorph.MDifferentiable.mfderiv_surjective

---

← Back to Index