ContDiff

📁 Source: Mathlib/Analysis/Calculus/InverseFunctionTheorem/ContDiff.lean

Statistics

Metric	Count
Definitions localInverse, toOpenPartialHomeomorph	2
Theorems image_mem_toOpenPartialHomeomorph_target, localInverse_apply_image, mem_toOpenPartialHomeomorph_source, toOpenPartialHomeomorph_coe, to_localInverse	5
Total	7

ContDiffAt

Definitions

Name	Category	Theorems
localInverse 📖	CompOp	2 math math: localInverse_apply_image, to_localInverse
toOpenPartialHomeomorph 📖	CompOp	3 math math: image_mem_toOpenPartialHomeomorph_target, toOpenPartialHomeomorph_coe, mem_toOpenPartialHomeomorph_source

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_mem_toOpenPartialHomeomorph_target 📖	mathematical	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField HasFDerivAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousLinearEquiv.toContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	Set Set.instMembership PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toOpenPartialHomeomorph	—	RingHomInvPair.ids HasStrictFDerivAt.image_mem_toOpenPartialHomeomorph_target hasStrictFDerivAt'
localInverse_apply_image 📖	mathematical	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField HasFDerivAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousLinearEquiv.toContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	localInverse	—	RingHomInvPair.ids HasStrictFDerivAt.localInverse_apply_image hasStrictFDerivAt'
mem_toOpenPartialHomeomorph_source 📖	mathematical	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField HasFDerivAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousLinearEquiv.toContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toOpenPartialHomeomorph	—	RingHomInvPair.ids HasStrictFDerivAt.mem_toOpenPartialHomeomorph_source hasStrictFDerivAt'
toOpenPartialHomeomorph_coe 📖	mathematical	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField HasFDerivAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousLinearEquiv.toContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	OpenPartialHomeomorph.toFun' UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toOpenPartialHomeomorph	—	RingHomInvPair.ids
to_localInverse 📖	mathematical	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField HasFDerivAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousLinearEquiv.toContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField localInverse	—	RingHomInvPair.ids localInverse_apply_image OpenPartialHomeomorph.contDiffAt_symm image_mem_toOpenPartialHomeomorph_target

---

← Back to Index