ContDiff

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

Statistics

Metric	Count
Definitions localInverse, toOpenPartialHomeomorph, toPartialHomeomorph	3
Theorems image_mem_toOpenPartialHomeomorph_target, image_mem_toPartialHomeomorph_target, localInverse_apply_image, mem_toOpenPartialHomeomorph_source, mem_toPartialHomeomorph_source, toOpenPartialHomeomorph_coe, toPartialHomeomorph_coe, to_localInverse	8
Total	11

ContDiffAt

Definitions

Name	Category	Theorems
localInverse 📖	CompOp	2 math math: localInverse_apply_image, to_localInverse
toOpenPartialHomeomorph 📖	CompOp	6 math math: image_mem_toOpenPartialHomeomorph_target, image_mem_toPartialHomeomorph_target, mem_toPartialHomeomorph_source, toOpenPartialHomeomorph_coe, mem_toOpenPartialHomeomorph_source, toPartialHomeomorph_coe
toPartialHomeomorph 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_mem_toOpenPartialHomeomorph_target 📖	mathematical	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField HasFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField 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 toOpenPartialHomeomorph	—	RingHomInvPair.ids HasStrictFDerivAt.image_mem_toOpenPartialHomeomorph_target hasStrictFDerivAt'
image_mem_toPartialHomeomorph_target 📖	mathematical	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField HasFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField 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 toOpenPartialHomeomorph	—	image_mem_toOpenPartialHomeomorph_target
localInverse_apply_image 📖	mathematical	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField HasFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField 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 SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField 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 toOpenPartialHomeomorph	—	RingHomInvPair.ids HasStrictFDerivAt.mem_toOpenPartialHomeomorph_source hasStrictFDerivAt'
mem_toPartialHomeomorph_source 📖	mathematical	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField HasFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField 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 toOpenPartialHomeomorph	—	mem_toOpenPartialHomeomorph_source
toOpenPartialHomeomorph_coe 📖	mathematical	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField HasFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField 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' toOpenPartialHomeomorph	—	RingHomInvPair.ids
toPartialHomeomorph_coe 📖	mathematical	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField HasFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField 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' toOpenPartialHomeomorph	—	toOpenPartialHomeomorph_coe
to_localInverse 📖	mathematical	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField HasFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField 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 localInverse_apply_image OpenPartialHomeomorph.contDiffAt_symm image_mem_toOpenPartialHomeomorph_target

---

← Back to Index