Documentation Verification Report

Atlas

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

Statistics

Metric	Count
Definitions `mfderiv`	1
Theorems `hasMFDerivAt`, `hasMFDerivWithinAt`, `hasMFDerivWithinAt_symm`, `mdifferentiable`, `mdifferentiableAt`, `mdifferentiableOn`, `mdifferentiableOn_symm`, `mdifferentiableWithinAt`, `mdifferentiableWithinAt_symm`, `comp_symm_deriv`, `ker_mfderiv_eq_bot`, `mdifferentiableAt`, `mdifferentiableAt_symm`, `mfderiv_bijective`, `mfderiv_injective`, `mfderiv_surjective`, `range_mfderiv_eq_top`, `range_mfderiv_eq_univ`, `symm_comp_deriv`, `trans`, `continuousLinearMapAt_trivializationAt`, `symmL_trivializationAt`, `hasMFDerivAt_extChartAt`, `hasMFDerivWithinAt_extChartAt`, `isInvertible_mfderivWithin_extChartAt_symm`, `isInvertible_mfderiv_extChartAt`, `mdifferentiableAt_atlas`, `mdifferentiableAt_atlas_symm`, `mdifferentiableAt_extChartAt`, `mdifferentiableOn_atlas`, `mdifferentiableOn_atlas_symm`, `mdifferentiableOn_extChartAt`, `mdifferentiableOn_extChartAt_symm`, `mdifferentiableWithinAt_extChartAt_symm`, `mdifferentiable_chart`, `mdifferentiable_of_mem_atlas`, `mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt`, `mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt'`, `mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm`, `mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm'`	40
Total	41

ModelWithCorners

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasMFDerivAt` 📖	mathematical	—	`HasMFDerivAt` `chartedSpaceSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `toFun'` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`continuousAt` `HasFDerivWithinAt.congr'` `hasFDerivWithinAt_id` `rightInvOn` `Set.mem_range_self`
`hasMFDerivWithinAt` 📖	mathematical	—	`HasMFDerivWithinAt` `chartedSpaceSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `toFun'` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`HasMFDerivAt.hasMFDerivWithinAt` `hasMFDerivAt`
`hasMFDerivWithinAt_symm` 📖	mathematical	`Set` `Set.instMembership` `Set.range` `toFun'`	`HasMFDerivWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `symm` `ContinuousLinearMap.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace`	—	`continuousWithinAt_symm` `HasFDerivWithinAt.congr'` `hasFDerivWithinAt_id` `rightInvOn` `Set.mem_range_self`
`mdifferentiable` 📖	mathematical	—	`MDifferentiable` `chartedSpaceSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `toFun'`	—	`mdifferentiableAt`
`mdifferentiableAt` 📖	mathematical	—	`MDifferentiableAt` `chartedSpaceSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `toFun'`	—	`HasMFDerivAt.mdifferentiableAt` `hasMFDerivAt`
`mdifferentiableOn` 📖	mathematical	—	`MDifferentiableOn` `chartedSpaceSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `toFun'`	—	`mdifferentiableWithinAt`
`mdifferentiableOn_symm` 📖	mathematical	—	`MDifferentiableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `symm` `Set.range` `toFun'`	—	`HasMFDerivWithinAt.mdifferentiableWithinAt` `hasMFDerivWithinAt_symm`
`mdifferentiableWithinAt` 📖	mathematical	—	`MDifferentiableWithinAt` `chartedSpaceSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `toFun'`	—	`HasMFDerivWithinAt.mdifferentiableWithinAt` `hasMFDerivWithinAt`
`mdifferentiableWithinAt_symm` 📖	mathematical	`Set` `Set.instMembership` `Set.range` `toFun'`	`MDifferentiableWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `symm`	—	`mdifferentiableOn_symm`

OpenPartialHomeomorph.MDifferentiable

Definitions

Name	Category	Theorems
`mfderiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_symm_deriv` 📖	mathematical	`OpenPartialHomeomorph.MDifferentiable` `Set` `Set.instMembership` `PartialEquiv.target` `OpenPartialHomeomorph.toPartialEquiv`	`ContinuousLinearMap.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `OpenPartialHomeomorph.toFun'` `OpenPartialHomeomorph.symm` `instModuleTangentSpace` `RingHomCompTriple.ids` `mfderiv` `ContinuousLinearMap.id`	—	`symm_comp_deriv` `symm`
`ker_mfderiv_eq_bot` 📖	mathematical	`OpenPartialHomeomorph.MDifferentiable` `Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv`	`LinearMap.ker` `TangentSpace` `OpenPartialHomeomorph.toFun'` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `instTopologicalSpaceTangentSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.toLinearMap` `mfderiv` `Bot.bot` `Submodule` `Submodule.instBot`	—	`LinearEquiv.ker` `RingHomInvPair.ids`
`mdifferentiableAt` 📖	mathematical	`OpenPartialHomeomorph.MDifferentiable` `Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv`	`MDifferentiableAt` `OpenPartialHomeomorph.toFun'`	—	`MDifferentiableWithinAt.mdifferentiableAt` `IsOpen.mem_nhds` `OpenPartialHomeomorph.open_source`
`mdifferentiableAt_symm` 📖	mathematical	`OpenPartialHomeomorph.MDifferentiable` `Set` `Set.instMembership` `PartialEquiv.target` `OpenPartialHomeomorph.toPartialEquiv`	`MDifferentiableAt` `OpenPartialHomeomorph.toFun'` `OpenPartialHomeomorph.symm`	—	`MDifferentiableWithinAt.mdifferentiableAt` `IsOpen.mem_nhds` `OpenPartialHomeomorph.open_target`
`mfderiv_bijective` 📖	mathematical	`OpenPartialHomeomorph.MDifferentiable` `Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv`	`Function.Bijective` `TangentSpace` `OpenPartialHomeomorph.toFun'` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.funLike` `mfderiv`	—	`ContinuousLinearEquiv.bijective` `RingHomInvPair.ids`
`mfderiv_injective` 📖	mathematical	`OpenPartialHomeomorph.MDifferentiable` `Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv`	`TangentSpace` `OpenPartialHomeomorph.toFun'` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.funLike` `mfderiv`	—	`ContinuousLinearEquiv.injective` `RingHomInvPair.ids`
`mfderiv_surjective` 📖	mathematical	`OpenPartialHomeomorph.MDifferentiable` `Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv`	`TangentSpace` `OpenPartialHomeomorph.toFun'` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.funLike` `mfderiv`	—	`ContinuousLinearEquiv.surjective` `RingHomInvPair.ids`
`range_mfderiv_eq_top` 📖	mathematical	`OpenPartialHomeomorph.MDifferentiable` `Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv`	`LinearMap.range` `TangentSpace` `OpenPartialHomeomorph.toFun'` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `instTopologicalSpaceTangentSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `ContinuousLinearMap.toLinearMap` `mfderiv` `Top.top` `Submodule` `Submodule.instTop`	—	`LinearEquiv.range` `RingHomInvPair.ids`
`range_mfderiv_eq_univ` 📖	mathematical	`OpenPartialHomeomorph.MDifferentiable` `Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv`	`Set.range` `TangentSpace` `OpenPartialHomeomorph.toFun'` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.funLike` `mfderiv` `Set.univ`	—	`Function.Surjective.range_eq` `mfderiv_surjective`
`symm_comp_deriv` 📖	mathematical	`OpenPartialHomeomorph.MDifferentiable` `Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv`	`ContinuousLinearMap.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `OpenPartialHomeomorph.toFun'` `OpenPartialHomeomorph.symm` `instModuleTangentSpace` `RingHomCompTriple.ids` `mfderiv` `ContinuousLinearMap.id`	—	`RingHomCompTriple.ids` `mfderiv_comp` `mdifferentiableAt_symm` `OpenPartialHomeomorph.map_source` `mdifferentiableAt` `mfderiv_id` `Filter.EventuallyEq.mfderiv_eq` `IsOpen.mem_nhds` `OpenPartialHomeomorph.open_source` `Filter.mem_of_superset` `OpenPartialHomeomorph.left_inv`
`trans` 📖	mathematical	`OpenPartialHomeomorph.MDifferentiable`	`OpenPartialHomeomorph.trans`	—	`MDifferentiableAt.mdifferentiableWithinAt` `MDifferentiableAt.comp` `mdifferentiableAt` `symm`

TangentBundle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousLinearMapAt_trivializationAt` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt`	`Trivialization.continuousLinearMapAt` `TangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `instTopologicalSpaceTangentSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `instTopologicalSpaceTangentBundle` `TangentSpace.fiberBundle` `FiberBundle.trivializationAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `trivialization_linear` `TangentSpace.vectorBundle` `instMemTrivializationAtlasTrivializationAt` `mfderiv` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `extChartAt`	—	`mdifferentiableAt_extChartAt` `trivialization_linear` `TangentSpace.vectorBundle` `instMemTrivializationAtlasTrivializationAt` `VectorBundleCore.trivializationAt_continuousLinearMapAt` `PartialEquiv.trans_refl` `CompTriple.comp_eq` `CompTriple.instId_comp` `CompTriple.instIsIdId`
`symmL_trivializationAt` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt`	`Trivialization.symmL` `TangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `instTopologicalSpaceTangentSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `instTopologicalSpaceTangentBundle` `TangentSpace.fiberBundle` `FiberBundle.trivializationAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `trivialization_linear` `TangentSpace.vectorBundle` `instMemTrivializationAtlasTrivializationAt` `mfderivWithin` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt` `Set.range` `ModelWithCorners.toFun'`	—	`mdifferentiableWithinAt_extChartAt_symm` `ModelWithCorners.target_eq` `ModelWithCorners.left_inv` `trivialization_linear` `TangentSpace.vectorBundle` `instMemTrivializationAtlasTrivializationAt` `VectorBundleCore.trivializationAt_symmL` `OpenPartialHomeomorph.left_inv` `PartialEquiv.trans_refl` `CompTriple.comp_eq` `CompTriple.instComp_id` `CompTriple.instIsIdId` `Set.range_id` `Set.inter_univ`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasMFDerivAt_extChartAt` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt`	`HasMFDerivAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `extChartAt` `mfderiv` `OpenPartialHomeomorph.toFun'`	—	`HasMFDerivAt.comp` `ModelWithCorners.hasMFDerivAt` `MDifferentiableAt.hasMFDerivAt` `OpenPartialHomeomorph.MDifferentiable.mdifferentiableAt` `mdifferentiable_chart`
`hasMFDerivWithinAt_extChartAt` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt`	`HasMFDerivWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `extChartAt` `mfderiv` `OpenPartialHomeomorph.toFun'`	—	`HasMFDerivAt.hasMFDerivWithinAt` `hasMFDerivAt_extChartAt`
`isInvertible_mfderivWithin_extChartAt_symm` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `extChartAt`	`ContinuousLinearMap.IsInvertible` `TangentSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `PartialEquiv.symm` `instTopologicalSpaceTangentSpace` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderivWithin` `Set.range` `ModelWithCorners.toFun'`	—	`ContinuousLinearMap.IsInvertible.of_inverse` `mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt` `mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm`
`isInvertible_mfderiv_extChartAt` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `extChartAt`	`ContinuousLinearMap.IsInvertible` `TangentSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `instTopologicalSpaceTangentSpace` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderiv`	—	`PartialEquiv.map_source` `ContinuousLinearMap.IsInvertible.of_inverse` `mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm` `mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt` `PartialEquiv.left_inv`
`mdifferentiableAt_atlas` 📖	mathematical	`OpenPartialHomeomorph` `Set` `Set.instMembership` `atlas` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv`	`MDifferentiableAt` `chartedSpaceSelf` `OpenPartialHomeomorph.toFun'`	—	`mdifferentiableAt_iff` `ContinuousWithinAt.continuousAt` `OpenPartialHomeomorph.continuousOn` `IsOpen.mem_nhds` `OpenPartialHomeomorph.open_source` `ModelWithCorners.left_inv` `OpenPartialHomeomorph.left_inv` `HasGroupoid.compatible` `IsManifold.toHasGroupoid` `chart_mem_atlas` `ContDiffOn.differentiableOn` `one_ne_zero` `NeZero.charZero_one` `WithTop.charZero` `PartialEquiv.refl_trans` `differentiableWithinAt_inter` `IsOpen.preimage` `ModelWithCorners.continuous_symm` `Set.inter_comm`
`mdifferentiableAt_atlas_symm` 📖	mathematical	`OpenPartialHomeomorph` `Set` `Set.instMembership` `atlas` `PartialEquiv.target` `OpenPartialHomeomorph.toPartialEquiv`	`MDifferentiableAt` `chartedSpaceSelf` `OpenPartialHomeomorph.toFun'` `OpenPartialHomeomorph.symm`	—	`mdifferentiableAt_iff` `ContinuousWithinAt.continuousAt` `OpenPartialHomeomorph.continuousOn_symm` `IsOpen.mem_nhds` `OpenPartialHomeomorph.open_target` `ModelWithCorners.left_inv` `HasGroupoid.compatible` `IsManifold.toHasGroupoid` `chart_mem_atlas` `ContDiffOn.differentiableOn` `one_ne_zero` `NeZero.charZero_one` `WithTop.charZero` `PartialEquiv.refl_trans` `differentiableWithinAt_inter` `IsOpen.preimage` `ModelWithCorners.continuous_symm` `OpenPartialHomeomorph.open_source` `Set.inter_comm`
`mdifferentiableAt_extChartAt` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt`	`MDifferentiableAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `extChartAt`	—	`HasMFDerivAt.mdifferentiableAt` `hasMFDerivAt_extChartAt`
`mdifferentiableOn_atlas` 📖	mathematical	`OpenPartialHomeomorph` `Set` `Set.instMembership` `atlas`	`MDifferentiableOn` `chartedSpaceSelf` `OpenPartialHomeomorph.toFun'` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv`	—	`MDifferentiableAt.mdifferentiableWithinAt` `mdifferentiableAt_atlas`
`mdifferentiableOn_atlas_symm` 📖	mathematical	`OpenPartialHomeomorph` `Set` `Set.instMembership` `atlas`	`MDifferentiableOn` `chartedSpaceSelf` `OpenPartialHomeomorph.toFun'` `OpenPartialHomeomorph.symm` `PartialEquiv.target` `OpenPartialHomeomorph.toPartialEquiv`	—	`MDifferentiableAt.mdifferentiableWithinAt` `mdifferentiableAt_atlas_symm`
`mdifferentiableOn_extChartAt` 📖	mathematical	—	`MDifferentiableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `extChartAt` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt`	—	`HasMFDerivWithinAt.mdifferentiableWithinAt` `hasMFDerivWithinAt_extChartAt`
`mdifferentiableOn_extChartAt_symm` 📖	mathematical	—	`MDifferentiableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt` `PartialEquiv.target`	—	`MDifferentiableWithinAt.mono` `extChartAt_target_subset_range` `mdifferentiableWithinAt_extChartAt_symm`
`mdifferentiableWithinAt_extChartAt_symm` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `extChartAt`	`MDifferentiableWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `PartialEquiv.symm` `Set.range` `ModelWithCorners.toFun'`	—	`ModelWithCorners.mdifferentiableWithinAt_symm` `extChartAt_target_subset_range` `MDifferentiableAt.comp_mdifferentiableWithinAt` `mdifferentiableAt_atlas_symm` `ChartedSpace.chart_mem_atlas` `ModelWithCorners.target_eq`
`mdifferentiable_chart` 📖	mathematical	—	`OpenPartialHomeomorph.MDifferentiable` `chartedSpaceSelf` `chartAt`	—	`mdifferentiable_of_mem_atlas` `chart_mem_atlas`
`mdifferentiable_of_mem_atlas` 📖	mathematical	`OpenPartialHomeomorph` `Set` `Set.instMembership` `atlas`	`OpenPartialHomeomorph.MDifferentiable` `chartedSpaceSelf`	—	`mdifferentiableOn_atlas` `mdifferentiableOn_atlas_symm`
`mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `extChartAt`	`ContinuousLinearMap.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `PartialEquiv.toFun` `PartialEquiv.symm` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `instModuleTangentSpace` `RingHomCompTriple.ids` `mfderivWithin` `Set.range` `ModelWithCorners.toFun'` `mfderiv` `ContinuousLinearMap.id`	—	`PartialEquiv.map_target` `extChartAt_source` `IsOpen.uniqueMDiffWithinAt` `isOpen_extChartAt_source` `mfderivWithin_eq_mfderiv` `mdifferentiableAt_extChartAt` `RingHomCompTriple.ids` `mfderivWithin_comp_of_eq` `mdifferentiableWithinAt_extChartAt_symm` `MDifferentiableAt.mdifferentiableWithinAt` `extChartAt_target_subset_range` `PartialEquiv.map_source` `PartialEquiv.right_inv` `mfderivWithin_id` `Filter.EventuallyEq.mfderivWithin_eq` `Filter.mp_mem` `extChartAt_source_mem_nhdsWithin'` `Filter.univ_mem'` `PartialEquiv.left_inv`
`mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt'` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `extChartAt`	`ContinuousLinearMap.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `PartialEquiv.symm` `instModuleTangentSpace` `RingHomCompTriple.ids` `mfderivWithin` `Set.range` `ModelWithCorners.toFun'` `mfderiv` `ContinuousLinearMap.id`	—	`PartialEquiv.left_inv` `RingHomCompTriple.ids` `mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt` `PartialEquiv.map_source`
`mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `extChartAt`	`ContinuousLinearMap.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `PartialEquiv.toFun` `PartialEquiv.symm` `instModuleTangentSpace` `RingHomCompTriple.ids` `mfderiv` `mfderivWithin` `Set.range` `ModelWithCorners.toFun'` `ContinuousLinearMap.id`	—	`ModelWithCorners.uniqueMDiffOn` `extChartAt_target_subset_range` `PartialEquiv.map_target` `extChartAt_source` `RingHomCompTriple.ids` `mfderiv_comp_mfderivWithin` `mdifferentiableAt_extChartAt` `mdifferentiableWithinAt_extChartAt_symm` `mfderivWithin_id` `Filter.EventuallyEq.mfderivWithin_eq` `Filter.mp_mem` `extChartAt_target_mem_nhdsWithin_of_mem` `Filter.univ_mem'` `PartialEquiv.right_inv`
`mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm'` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `extChartAt`	`ContinuousLinearMap.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `RingHomCompTriple.ids` `mfderiv` `mfderivWithin` `PartialEquiv.symm` `Set.range` `ModelWithCorners.toFun'` `ContinuousLinearMap.id`	—	`PartialEquiv.left_inv` `RingHomCompTriple.ids` `mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm` `PartialEquiv.map_source`

---

← Back to Index