Documentation Verification Report

LocalDiffeomorph

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

Statistics

Metric	Count
Definitions `mfderivToContinuousLinearEquiv`, `toPartialDiffeomorph`, `IsLocalDiffeomorph`, `diffeomorphOfBijective`, `diffeomorph_of_bijective`, `image`, `mfderivToContinuousLinearEquiv`, `IsLocalDiffeomorphAt`, `localInverse`, `mfderivToContinuousLinearEquiv`, `IsLocalDiffeomorphOn`, `PartialDiffeomorph`, `toOpenPartialHomeomorph`, `toPartialEquiv`, `instCoeFunPartialDiffeomorphForall`	15
Theorems `isLocalDiffeomorph`, `mfderivToContinuousLinearEquiv_coe`, `contMDiff`, `image_coe`, `isLocalDiffeomorphOn`, `isLocalHomeomorph`, `isOpenMap`, `isOpen_range`, `mdifferentiable`, `mfderivToContinuousLinearEquiv_coe`, `contMDiffAt`, `contmdiffOn_localInverse`, `localInverse_contMDiffAt`, `localInverse_contMDiffOn`, `localInverse_eqOn_left`, `localInverse_eqOn_right`, `localInverse_eventuallyEq_left`, `localInverse_eventuallyEq_right`, `localInverse_isLocalDiffeomorphAt`, `localInverse_left_inv`, `localInverse_mdifferentiableAt`, `localInverse_mem_source`, `localInverse_mem_target`, `localInverse_open_source`, `localInverse_right_inv`, `mdifferentiableAt`, `mfderivToContinuousLinearEquiv_coe`, `contMDiffOn`, `isLocalHomeomorphOn`, `mdifferentiableOn`, `contMDiffOn`, `contMDiffOn_invFun`, `contMDiffOn_toFun`, `isLocalDiffeomorphAt`, `mdifferentiableAt`, `mdifferentiableOn`, `open_source`, `open_target`, `isLocalDiffeomorphOn_iff`, `isLocalDiffeomorph_iff`, `isLocalDiffeomorph_iff_isLocalDiffeomorphOn_univ`	41
Total	56

Diffeomorph

Definitions

Name	Category	Theorems
`mfderivToContinuousLinearEquiv` 📖	CompOp	1 math math: `mfderivToContinuousLinearEquiv_coe`
`toPartialDiffeomorph` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocalDiffeomorph` 📖	mathematical	—	`IsLocalDiffeomorph` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`Set.eqOn_refl`
`mfderivToContinuousLinearEquiv_coe` 📖	mathematical	—	`ContinuousLinearEquiv.toContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike` `instModuleTangentSpace` `mfderivToContinuousLinearEquiv` `mfderiv`	—	`RingHomInvPair.ids`

IsLocalDiffeomorph

Definitions

Name	Category	Theorems
`diffeomorphOfBijective` 📖	CompOp	—
`diffeomorph_of_bijective` 📖	CompOp	—
`image` 📖	CompOp	1 math math: `image_coe`
`mfderivToContinuousLinearEquiv` 📖	CompOp	1 math math: `mfderivToContinuousLinearEquiv_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contMDiff` 📖	mathematical	`IsLocalDiffeomorph`	`ContMDiff`	—	`IsLocalDiffeomorphAt.contMDiffAt`
`image_coe` 📖	mathematical	`IsLocalDiffeomorph`	`TopologicalSpace.Opens.carrier` `image` `Set.range`	—	—
`isLocalDiffeomorphOn` 📖	mathematical	`IsLocalDiffeomorph`	`IsLocalDiffeomorphOn`	—	—
`isLocalHomeomorph` 📖	mathematical	`IsLocalDiffeomorph`	`IsLocalHomeomorph`	—	`isLocalHomeomorph_iff_isLocalHomeomorphOn_univ` `IsLocalDiffeomorphOn.isLocalHomeomorphOn` `isLocalDiffeomorph_iff_isLocalDiffeomorphOn_univ`
`isOpenMap` 📖	mathematical	`IsLocalDiffeomorph`	`IsOpenMap`	—	`IsLocalHomeomorph.isOpenMap` `isLocalHomeomorph`
`isOpen_range` 📖	mathematical	`IsLocalDiffeomorph`	`IsOpen` `Set.range`	—	`IsOpenMap.isOpen_range` `isOpenMap`
`mdifferentiable` 📖	mathematical	`IsLocalDiffeomorph`	`MDifferentiable`	—	`IsLocalDiffeomorphAt.mdifferentiableAt`
`mfderivToContinuousLinearEquiv_coe` 📖	mathematical	`IsLocalDiffeomorph`	`ContinuousLinearEquiv.toContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderivToContinuousLinearEquiv` `mfderiv`	—	`IsLocalDiffeomorphAt.mfderivToContinuousLinearEquiv_coe`

IsLocalDiffeomorphAt

Definitions

Name	Category	Theorems
`localInverse` 📖	CompOp	14 math math: `localInverse_eventuallyEq_right`, `localInverse_mdifferentiableAt`, `localInverse_contMDiffOn`, `localInverse_mem_target`, `contmdiffOn_localInverse`, `localInverse_open_source`, `localInverse_eqOn_right`, `localInverse_eventuallyEq_left`, `localInverse_isLocalDiffeomorphAt`, `localInverse_contMDiffAt`, `localInverse_left_inv`, `localInverse_right_inv`, `localInverse_mem_source`, `localInverse_eqOn_left`
`mfderivToContinuousLinearEquiv` 📖	CompOp	1 math math: `mfderivToContinuousLinearEquiv_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contMDiffAt` 📖	mathematical	`IsLocalDiffeomorphAt`	`ContMDiffAt`	—	`ContMDiffOn.contMDiffAt` `ContMDiffOn.congr` `PartialDiffeomorph.contMDiffOn_toFun` `IsOpen.mem_nhds` `PartialDiffeomorph.open_source`
`contmdiffOn_localInverse` 📖	mathematical	`IsLocalDiffeomorphAt`	`ContMDiffOn` `PartialEquiv.toFun` `PartialDiffeomorph.toPartialEquiv` `localInverse` `PartialEquiv.source`	—	`PartialDiffeomorph.contMDiffOn_toFun`
`localInverse_contMDiffAt` 📖	mathematical	`IsLocalDiffeomorphAt`	`ContMDiffAt` `PartialEquiv.toFun` `PartialDiffeomorph.toPartialEquiv` `localInverse`	—	`ContMDiffOn.contMDiffAt` `localInverse_contMDiffOn` `IsOpen.mem_nhds` `PartialDiffeomorph.open_source` `localInverse_mem_source`
`localInverse_contMDiffOn` 📖	mathematical	`IsLocalDiffeomorphAt`	`ContMDiffOn` `PartialEquiv.toFun` `PartialDiffeomorph.toPartialEquiv` `localInverse` `PartialEquiv.source`	—	`PartialDiffeomorph.contMDiffOn_toFun`
`localInverse_eqOn_left` 📖	mathematical	`IsLocalDiffeomorphAt`	`Set.EqOn` `PartialEquiv.toFun` `PartialDiffeomorph.toPartialEquiv` `localInverse` `PartialEquiv.target`	—	`localInverse_left_inv`
`localInverse_eqOn_right` 📖	mathematical	`IsLocalDiffeomorphAt`	`Set.EqOn` `PartialEquiv.toFun` `PartialDiffeomorph.toPartialEquiv` `localInverse` `PartialEquiv.source`	—	`localInverse_right_inv`
`localInverse_eventuallyEq_left` 📖	mathematical	`IsLocalDiffeomorphAt`	`Filter.EventuallyEq` `nhds` `PartialEquiv.toFun` `PartialDiffeomorph.toPartialEquiv` `localInverse`	—	`Filter.eventuallyEq_of_mem` `IsOpen.mem_nhds` `PartialDiffeomorph.open_target` `localInverse_mem_target` `localInverse_eqOn_left`
`localInverse_eventuallyEq_right` 📖	mathematical	`IsLocalDiffeomorphAt`	`Filter.EventuallyEq` `nhds` `PartialEquiv.toFun` `PartialDiffeomorph.toPartialEquiv` `localInverse`	—	`Filter.eventuallyEq_of_mem` `IsOpen.mem_nhds` `PartialDiffeomorph.open_source` `localInverse_mem_source` `localInverse_eqOn_right`
`localInverse_isLocalDiffeomorphAt` 📖	mathematical	`IsLocalDiffeomorphAt`	`IsLocalDiffeomorphAt` `PartialEquiv.toFun` `PartialDiffeomorph.toPartialEquiv` `localInverse`	—	`PartialDiffeomorph.isLocalDiffeomorphAt` `localInverse_mem_source`
`localInverse_left_inv` 📖	mathematical	`IsLocalDiffeomorphAt` `Set` `Set.instMembership` `PartialEquiv.target` `PartialDiffeomorph.toPartialEquiv` `localInverse`	`PartialEquiv.toFun` `PartialDiffeomorph.toPartialEquiv` `localInverse`	—	`PartialEquiv.symm_target` `PartialEquiv.left_inv`
`localInverse_mdifferentiableAt` 📖	mathematical	`IsLocalDiffeomorphAt`	`MDifferentiableAt` `PartialEquiv.toFun` `PartialDiffeomorph.toPartialEquiv` `localInverse`	—	`ContMDiffAt.mdifferentiableAt` `localInverse_contMDiffAt`
`localInverse_mem_source` 📖	mathematical	`IsLocalDiffeomorphAt`	`Set` `Set.instMembership` `PartialEquiv.source` `PartialDiffeomorph.toPartialEquiv` `localInverse`	—	`PartialEquiv.map_source`
`localInverse_mem_target` 📖	mathematical	`IsLocalDiffeomorphAt`	`Set` `Set.instMembership` `PartialEquiv.target` `PartialDiffeomorph.toPartialEquiv` `localInverse`	—	—
`localInverse_open_source` 📖	mathematical	`IsLocalDiffeomorphAt`	`IsOpen` `PartialEquiv.source` `PartialDiffeomorph.toPartialEquiv` `localInverse`	—	`PartialDiffeomorph.open_source`
`localInverse_right_inv` 📖	mathematical	`IsLocalDiffeomorphAt` `Set` `Set.instMembership` `PartialEquiv.source` `PartialDiffeomorph.toPartialEquiv` `localInverse`	`PartialEquiv.toFun` `PartialDiffeomorph.toPartialEquiv` `localInverse`	—	`PartialEquiv.symm_target` `PartialEquiv.map_source` `PartialEquiv.right_inv`
`mdifferentiableAt` 📖	mathematical	`IsLocalDiffeomorphAt`	`MDifferentiableAt`	—	`ContMDiffAt.mdifferentiableAt` `contMDiffAt`
`mfderivToContinuousLinearEquiv_coe` 📖	mathematical	`IsLocalDiffeomorphAt`	`ContinuousLinearEquiv.toContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderivToContinuousLinearEquiv` `mfderiv`	—	`RingHomInvPair.ids`

IsLocalDiffeomorphOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contMDiffOn` 📖	mathematical	`IsLocalDiffeomorphOn`	`ContMDiffOn`	—	`ContMDiffAt.contMDiffWithinAt` `IsLocalDiffeomorphAt.contMDiffAt`
`isLocalHomeomorphOn` 📖	mathematical	`IsLocalDiffeomorphOn`	`IsLocalHomeomorphOn`	—	—
`mdifferentiableOn` 📖	mathematical	`IsLocalDiffeomorphOn`	`MDifferentiableOn`	—	`ContMDiffOn.mdifferentiableOn` `contMDiffOn`

PartialDiffeomorph

Definitions

Name	Category	Theorems
`toOpenPartialHomeomorph` 📖	CompOp	—
`toPartialEquiv` 📖	CompOp	22 math math: `IsLocalDiffeomorphAt.localInverse_eventuallyEq_right`, `contMDiffOn`, `IsLocalDiffeomorphAt.localInverse_mdifferentiableAt`, `contMDiffOn_toFun`, `isLocalDiffeomorphAt`, `IsLocalDiffeomorphAt.localInverse_contMDiffOn`, `IsLocalDiffeomorphAt.localInverse_mem_target`, `IsLocalDiffeomorphAt.contmdiffOn_localInverse`, `IsLocalDiffeomorphAt.localInverse_open_source`, `IsLocalDiffeomorphAt.localInverse_eqOn_right`, `IsLocalDiffeomorphAt.localInverse_eventuallyEq_left`, `IsLocalDiffeomorphAt.localInverse_isLocalDiffeomorphAt`, `mdifferentiableOn`, `IsLocalDiffeomorphAt.localInverse_contMDiffAt`, `IsLocalDiffeomorphAt.localInverse_left_inv`, `IsLocalDiffeomorphAt.localInverse_right_inv`, `mdifferentiableAt`, `contMDiffOn_invFun`, `IsLocalDiffeomorphAt.localInverse_mem_source`, `open_target`, `open_source`, `IsLocalDiffeomorphAt.localInverse_eqOn_left`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contMDiffOn` 📖	mathematical	—	`ContMDiffOn` `PartialEquiv.toFun` `toPartialEquiv` `PartialEquiv.source`	—	`contMDiffOn_toFun`
`contMDiffOn_invFun` 📖	mathematical	—	`ContMDiffOn` `PartialEquiv.invFun` `toPartialEquiv` `PartialEquiv.target`	—	—
`contMDiffOn_toFun` 📖	mathematical	—	`ContMDiffOn` `PartialEquiv.toFun` `toPartialEquiv` `PartialEquiv.source`	—	—
`isLocalDiffeomorphAt` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv`	`IsLocalDiffeomorphAt` `PartialEquiv.toFun` `toPartialEquiv`	—	`Set.eqOn_refl`
`mdifferentiableAt` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `toPartialEquiv`	`MDifferentiableAt` `PartialEquiv.toFun` `toPartialEquiv`	—	`MDifferentiableWithinAt.mdifferentiableAt` `mdifferentiableOn` `IsOpen.mem_nhds` `open_source`
`mdifferentiableOn` 📖	mathematical	—	`MDifferentiableOn` `PartialEquiv.toFun` `toPartialEquiv` `PartialEquiv.source`	—	`ContMDiffOn.mdifferentiableOn` `contMDiffOn`
`open_source` 📖	mathematical	—	`IsOpen` `PartialEquiv.source` `toPartialEquiv`	—	—
`open_target` 📖	mathematical	—	`IsOpen` `PartialEquiv.target` `toPartialEquiv`	—	—

(root)

Definitions

Name	Category	Theorems
`IsLocalDiffeomorph` 📖	MathDef	3 math math: `isLocalDiffeomorph_iff_isLocalDiffeomorphOn_univ`, `Diffeomorph.isLocalDiffeomorph`, `isLocalDiffeomorph_iff`
`IsLocalDiffeomorphAt` 📖	MathDef	4 math math: `PartialDiffeomorph.isLocalDiffeomorphAt`, `isLocalDiffeomorph_iff`, `IsLocalDiffeomorphAt.localInverse_isLocalDiffeomorphAt`, `isLocalDiffeomorphOn_iff`
`IsLocalDiffeomorphOn` 📖	MathDef	3 math math: `isLocalDiffeomorph_iff_isLocalDiffeomorphOn_univ`, `IsLocalDiffeomorph.isLocalDiffeomorphOn`, `isLocalDiffeomorphOn_iff`
`PartialDiffeomorph` 📖	CompData	—
`instCoeFunPartialDiffeomorphForall` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocalDiffeomorphOn_iff` 📖	mathematical	—	`IsLocalDiffeomorphOn` `IsLocalDiffeomorphAt` `Set` `Set.instMembership`	—	—
`isLocalDiffeomorph_iff` 📖	mathematical	—	`IsLocalDiffeomorph` `IsLocalDiffeomorphAt`	—	—
`isLocalDiffeomorph_iff_isLocalDiffeomorphOn_univ` 📖	mathematical	—	`IsLocalDiffeomorph` `IsLocalDiffeomorphOn` `Set.univ`	—	—

---

← Back to Index