Diffeomorph

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

Statistics

Metric	Count
Definitions `toDiffeomorph`, `toTransContinuousLinearEquiv`, `Diffeomorph`, `empty`, `instCoeContMDiffMap`, `instEquivLike`, `prodAssoc`, `prodComm`, `prodCongr`, `refl`, `sumAssoc`, `sumComm`, `sumCongr`, `sumEmpty`, `toContMDiffMap`, `toEquiv`, `toHomeomorph`, `trans`, `«term_≃ₘ[_]_»`, `«term_≃ₘ^_[_]_»`, `«term_≃ₘ^_⟮_,_⟯_»`, `«term_≃ₘ⟮_,_⟯_»`, `transContinuousLinearEquiv`	23
Theorems `coe_toDiffeomorph`, `coe_toDiffeomorph_symm`, `contMDiffAt_transContinuousLinearEquiv_left`, `contMDiffAt_transContinuousLinearEquiv_right`, `contMDiffOn_transContinuousLinearEquiv_left`, `contMDiffOn_transContinuousLinearEquiv_right`, `contMDiffWithinAt_transContinuousLinearEquiv_left`, `contMDiffWithinAt_transContinuousLinearEquiv_right`, `contMDiff_transContinuousLinearEquiv_left`, `contMDiff_transContinuousLinearEquiv_right`, `instIsManifoldtransContinuousLinearEquiv`, `symm_toDiffeomorph`, `apply_symm_apply`, `coeFn_injective`, `coe_coe`, `coe_prodComm`, `coe_prodCongr`, `coe_refl`, `coe_toEquiv`, `coe_toHomeomorph`, `coe_toHomeomorph_symm`, `coe_trans`, `contDiff`, `contMDiff`, `contMDiffAt`, `contMDiffAt_comp_diffeomorph_iff`, `contMDiffAt_diffeomorph_comp_iff`, `contMDiffOn_comp_diffeomorph_iff`, `contMDiffOn_diffeomorph_comp_iff`, `contMDiffWithinAt`, `contMDiffWithinAt_comp_diffeomorph_iff`, `contMDiffWithinAt_diffeomorph_comp_iff`, `contMDiff_comp_diffeomorph_iff`, `contMDiff_diffeomorph_comp_iff`, `contMDiff_invFun`, `contMDiff_toFun`, `continuous`, `ext`, `ext_iff`, `image_eq_preimage_symm`, `image_symm_image`, `instContinuousMapClassSomeENatTop`, `mdifferentiable`, `mdifferentiableOn`, `prodComm_symm`, `prodCongr_symm`, `range_comp`, `refl_toEquiv`, `refl_trans`, `self_trans_symm`, `sumAssoc_coe`, `sumComm_coe`, `sumComm_inl`, `sumComm_inr`, `sumComm_symm`, `sumCongr_coe`, `sumCongr_inl`, `sumCongr_inr`, `sumCongr_symm_symm`, `sumEmpty_apply_inl`, `sumEmpty_toEquiv`, `symm_apply_apply`, `symm_image_eq_preimage`, `symm_image_image`, `symm_refl`, `symm_toEquiv`, `symm_toHomeomorph`, `symm_trans'`, `symm_trans_self`, `toEquiv_coe_symm`, `toEquiv_inj`, `toEquiv_injective`, `toHomeomorph_toEquiv`, `toOpenPartialHomeomorph_mdifferentiable`, `toPartialHomeomorph_mdifferentiable`, `trans_refl`, `uniqueDiffOn_image`, `uniqueDiffOn_preimage`, `uniqueMDiffOn_image`, `uniqueMDiffOn_image_aux`, `uniqueMDiffOn_preimage`, `coe_extChartAt_transContinuousLinearEquiv`, `coe_extChartAt_transContinuousLinearEquiv_symm`, `coe_transContinuousLinearEquiv`, `coe_transContinuousLinearEquiv_symm`, `extChartAt_transContinuousLinearEquiv_target`, `transContinuousLinearEquiv_range`	87
Total	110

ContinuousLinearEquiv

Definitions

Name	Category	Theorems
`toDiffeomorph` 📖	CompOp	3 math math: `symm_toDiffeomorph`, `coe_toDiffeomorph_symm`, `coe_toDiffeomorph`
`toTransContinuousLinearEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toDiffeomorph` 📖	mathematical	—	`DFunLike.coe` `Diffeomorph` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `WithTop.some` `ENat` `Top.top` `instTopENat` `EquivLike.toFunLike` `Diffeomorph.instEquivLike` `toDiffeomorph` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `equivLike`	—	`RingHomInvPair.ids`
`coe_toDiffeomorph_symm` 📖	mathematical	—	`DFunLike.coe` `Diffeomorph` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `WithTop.some` `ENat` `Top.top` `instTopENat` `EquivLike.toFunLike` `Diffeomorph.instEquivLike` `Diffeomorph.symm` `toDiffeomorph` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `equivLike` `symm`	—	`RingHomInvPair.ids`
`contMDiffAt_transContinuousLinearEquiv_left` 📖	mathematical	—	`ContMDiffAt` `ModelWithCorners.transContinuousLinearEquiv`	—	`RingHomInvPair.ids` `Diffeomorph.contMDiffAt_comp_diffeomorph_iff` `le_rfl`
`contMDiffAt_transContinuousLinearEquiv_right` 📖	mathematical	—	`ContMDiffAt` `ModelWithCorners.transContinuousLinearEquiv`	—	`RingHomInvPair.ids` `Diffeomorph.contMDiffAt_diffeomorph_comp_iff` `le_rfl`
`contMDiffOn_transContinuousLinearEquiv_left` 📖	mathematical	—	`ContMDiffOn` `ModelWithCorners.transContinuousLinearEquiv`	—	`RingHomInvPair.ids` `Diffeomorph.contMDiffOn_comp_diffeomorph_iff` `le_rfl`
`contMDiffOn_transContinuousLinearEquiv_right` 📖	mathematical	—	`ContMDiffOn` `ModelWithCorners.transContinuousLinearEquiv`	—	`RingHomInvPair.ids` `Diffeomorph.contMDiffOn_diffeomorph_comp_iff` `le_rfl`
`contMDiffWithinAt_transContinuousLinearEquiv_left` 📖	mathematical	—	`ContMDiffWithinAt` `ModelWithCorners.transContinuousLinearEquiv`	—	`RingHomInvPair.ids` `Diffeomorph.contMDiffWithinAt_comp_diffeomorph_iff` `le_rfl`
`contMDiffWithinAt_transContinuousLinearEquiv_right` 📖	mathematical	—	`ContMDiffWithinAt` `ModelWithCorners.transContinuousLinearEquiv`	—	`RingHomInvPair.ids` `Diffeomorph.contMDiffWithinAt_diffeomorph_comp_iff` `le_rfl`
`contMDiff_transContinuousLinearEquiv_left` 📖	mathematical	—	`ContMDiff` `ModelWithCorners.transContinuousLinearEquiv`	—	`RingHomInvPair.ids` `Diffeomorph.contMDiff_comp_diffeomorph_iff` `le_rfl`
`contMDiff_transContinuousLinearEquiv_right` 📖	mathematical	—	`ContMDiff` `ModelWithCorners.transContinuousLinearEquiv`	—	`RingHomInvPair.ids` `Diffeomorph.contMDiff_diffeomorph_comp_iff` `le_rfl`
`instIsManifoldtransContinuousLinearEquiv` 📖	mathematical	—	`IsManifold` `ModelWithCorners.transContinuousLinearEquiv`	—	`RingHomInvPair.ids` `isManifold_of_contDiffOn` `ContDiff.comp_contDiffOn` `contDiff` `ContDiffOn.comp` `StructureGroupoid.compatible` `IsManifold.toHasGroupoid` `ContDiff.contDiffOn` `ModelWithCorners.target_eq` `Set.range_comp` `image_eq_preimage_symm` `Set.instReflSubset`
`symm_toDiffeomorph` 📖	mathematical	—	`toDiffeomorph` `symm` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Diffeomorph.symm` `modelWithCornersSelf` `chartedSpaceSelf` `WithTop.some` `ENat` `Top.top` `instTopENat`	—	`RingHomInvPair.ids`

Diffeomorph

Definitions

Name	Category	Theorems
`empty` 📖	CompOp	—
`instCoeContMDiffMap` 📖	CompOp	—
`instEquivLike` 📖	CompOp	51 math math: `coe_refl`, `contMDiffWithinAt`, `contMDiffOn_comp_diffeomorph_iff`, `uniqueMDiffOn_preimage`, `ContinuousLinearEquiv.coe_toDiffeomorph_symm`, `apply_symm_apply`, `coe_coe`, `mdifferentiableOn`, `coe_prodCongr`, `contMDiff_comp_diffeomorph_iff`, `image_eq_preimage_symm`, `sumAssoc_coe`, `sumCongr_inl`, `range_comp`, `coeFn_injective`, `sumComm_coe`, `coe_trans`, `isLocalDiffeomorph`, `mfderivToContinuousLinearEquiv_coe`, `sumComm_inr`, `uniqueMDiffOn_image`, `contMDiffAt_diffeomorph_comp_iff`, `sumCongr_coe`, `symm_apply_apply`, `coe_prodComm`, `contDiff`, `symm_image_image`, `uniqueDiffOn_image`, `sumCongr_inr`, `contMDiffOn_diffeomorph_comp_iff`, `contMDiffAt_comp_diffeomorph_iff`, `mdifferentiable`, `sumEmpty_apply_inl`, `contMDiffWithinAt_comp_diffeomorph_iff`, `coe_toEquiv`, `uniqueMDiffOn_image_aux`, `continuous`, `contMDiffAt`, `symm_image_eq_preimage`, `uniqueDiffOn_preimage`, `instContinuousMapClassSomeENatTop`, `ContinuousLinearEquiv.coe_toDiffeomorph`, `contMDiffWithinAt_diffeomorph_comp_iff`, `ext_iff`, `contMDiff_diffeomorph_comp_iff`, `contMDiff`, `sumComm_inl`, `toEquiv_coe_symm`, `image_symm_image`, `coe_toHomeomorph_symm`, `coe_toHomeomorph`
`prodAssoc` 📖	CompOp	—
`prodComm` 📖	CompOp	2 math math: `coe_prodComm`, `prodComm_symm`
`prodCongr` 📖	CompOp	2 math math: `coe_prodCongr`, `prodCongr_symm`
`refl` 📖	CompOp	7 math math: `coe_refl`, `symm_refl`, `refl_trans`, `self_trans_symm`, `trans_refl`, `refl_toEquiv`, `symm_trans_self`
`sumAssoc` 📖	CompOp	1 math math: `sumAssoc_coe`
`sumComm` 📖	CompOp	4 math math: `sumComm_coe`, `sumComm_inr`, `sumComm_inl`, `sumComm_symm`
`sumCongr` 📖	CompOp	4 math math: `sumCongr_symm_symm`, `sumCongr_inl`, `sumCongr_coe`, `sumCongr_inr`
`sumEmpty` 📖	CompOp	2 math math: `sumEmpty_apply_inl`, `sumEmpty_toEquiv`
`toContMDiffMap` 📖	CompOp	1 math math: `coe_coe`
`toEquiv` 📖	CompOp	10 math math: `toEquiv_injective`, `contMDiff_toFun`, `toHomeomorph_toEquiv`, `contMDiff_invFun`, `symm_toEquiv`, `coe_toEquiv`, `sumEmpty_toEquiv`, `refl_toEquiv`, `toEquiv_coe_symm`, `toEquiv_inj`
`toHomeomorph` 📖	CompOp	6 math math: `toPartialHomeomorph_mdifferentiable`, `toOpenPartialHomeomorph_mdifferentiable`, `toHomeomorph_toEquiv`, `symm_toHomeomorph`, `coe_toHomeomorph_symm`, `coe_toHomeomorph`
`trans` 📖	CompOp	6 math math: `symm_trans'`, `refl_trans`, `coe_trans`, `self_trans_symm`, `trans_refl`, `symm_trans_self`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.apply_symm_apply`
`coeFn_injective` 📖	mathematical	—	`Diffeomorph` `DFunLike.coe` `EquivLike.toFunLike` `instEquivLike`	—	`DFunLike.coe_injective`
`coe_coe` 📖	mathematical	—	`DFunLike.coe` `ContMDiffMap` `ContMDiffMap.instFunLike` `toContMDiffMap` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike`	—	—
`coe_prodComm` 📖	mathematical	—	`DFunLike.coe` `Diffeomorph` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `EquivLike.toFunLike` `instEquivLike` `prodComm`	—	—
`coe_prodCongr` 📖	mathematical	—	`DFunLike.coe` `Diffeomorph` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `EquivLike.toFunLike` `instEquivLike` `prodCongr`	—	—
`coe_refl` 📖	mathematical	—	`DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike` `refl`	—	—
`coe_toEquiv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toEquiv` `Diffeomorph` `instEquivLike`	—	—
`coe_toHomeomorph` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `toHomeomorph` `Diffeomorph` `instEquivLike`	—	—
`coe_toHomeomorph_symm` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `toHomeomorph` `Diffeomorph` `instEquivLike` `symm`	—	—
`coe_trans` 📖	mathematical	—	`DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike` `trans`	—	—
`contDiff` 📖	mathematical	—	`ContDiff` `DFunLike.coe` `Diffeomorph` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `EquivLike.toFunLike` `instEquivLike`	—	`ContMDiff.contDiff` `contMDiff`
`contMDiff` 📖	mathematical	—	`ContMDiff` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`contMDiff_toFun`
`contMDiffAt` 📖	mathematical	—	`ContMDiffAt` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`ContMDiff.contMDiffAt` `contMDiff`
`contMDiffAt_comp_diffeomorph_iff` 📖	mathematical	`WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat`	`ContMDiffAt` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`contMDiffWithinAt_comp_diffeomorph_iff`
`contMDiffAt_diffeomorph_comp_iff` 📖	mathematical	`WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat`	`ContMDiffAt` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`contMDiffWithinAt_diffeomorph_comp_iff`
`contMDiffOn_comp_diffeomorph_iff` 📖	mathematical	`WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat`	`ContMDiffOn` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike` `Set.preimage` `symm`	—	`Equiv.forall_congr` `symm_apply_apply`
`contMDiffOn_diffeomorph_comp_iff` 📖	mathematical	`WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat`	`ContMDiffOn` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`contMDiffWithinAt_diffeomorph_comp_iff`
`contMDiffWithinAt` 📖	mathematical	—	`ContMDiffWithinAt` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`ContMDiffAt.contMDiffWithinAt` `contMDiffAt`
`contMDiffWithinAt_comp_diffeomorph_iff` 📖	mathematical	`WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat`	`ContMDiffWithinAt` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike` `Set.preimage` `symm`	—	`apply_symm_apply` `ContMDiffWithinAt.comp` `symm_apply_apply` `ContMDiffWithinAt.of_le` `contMDiffWithinAt` `Set.mapsTo_preimage` `image_eq_preimage_symm` `Set.mapsTo_image`
`contMDiffWithinAt_diffeomorph_comp_iff` 📖	mathematical	`WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat`	`ContMDiffWithinAt` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`symm_apply_apply` `ContMDiffAt.comp_contMDiffWithinAt` `ContMDiffAt.of_le` `contMDiffAt`
`contMDiff_comp_diffeomorph_iff` 📖	mathematical	`WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat`	`ContMDiff` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`Equiv.forall_congr` `contMDiffAt_comp_diffeomorph_iff`
`contMDiff_diffeomorph_comp_iff` 📖	mathematical	`WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat`	`ContMDiff` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`contMDiffWithinAt_diffeomorph_comp_iff`
`contMDiff_invFun` 📖	mathematical	—	`ContMDiff` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toEquiv`	—	—
`contMDiff_toFun` 📖	mathematical	—	`ContMDiff` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toEquiv`	—	—
`continuous` 📖	mathematical	—	`Continuous` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`ContMDiff.continuous` `contMDiff_toFun`
`ext` 📖	—	`DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike`	—	—	`coeFn_injective`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`ext`
`image_eq_preimage_symm` 📖	mathematical	—	`Set.image` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike` `Set.preimage` `symm`	—	`Equiv.image_eq_preimage_symm`
`image_symm_image` 📖	mathematical	—	`Set.image` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.image_symm_image`
`instContinuousMapClassSomeENatTop` 📖	mathematical	—	`ContinuousMapClass` `Diffeomorph` `WithTop.some` `ENat` `Top.top` `instTopENat` `EquivLike.toFunLike` `instEquivLike`	—	`continuous`
`mdifferentiable` 📖	mathematical	—	`MDifferentiable` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`ContMDiff.mdifferentiable` `contMDiff`
`mdifferentiableOn` 📖	mathematical	—	`MDifferentiableOn` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`MDifferentiable.mdifferentiableOn` `mdifferentiable`
`prodComm_symm` 📖	mathematical	—	`symm` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `prodComm`	—	—
`prodCongr_symm` 📖	mathematical	—	`symm` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `prodCongr`	—	—
`range_comp` 📖	mathematical	—	`Set.range` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike` `Set.preimage` `symm`	—	`Set.range_comp` `image_eq_preimage_symm`
`refl_toEquiv` 📖	mathematical	—	`toEquiv` `refl` `Equiv.refl`	—	—
`refl_trans` 📖	mathematical	—	`trans` `refl`	—	`ext`
`self_trans_symm` 📖	mathematical	—	`trans` `symm` `refl`	—	`ext` `symm_apply_apply`
`sumAssoc_coe` 📖	mathematical	—	`DFunLike.coe` `Diffeomorph` `instTopologicalSpaceSum` `ChartedSpace.sum` `EquivLike.toFunLike` `instEquivLike` `sumAssoc` `Equiv` `Equiv.instEquivLike` `Equiv.sumAssoc`	—	—
`sumComm_coe` 📖	mathematical	—	`DFunLike.coe` `Diffeomorph` `instTopologicalSpaceSum` `ChartedSpace.sum` `EquivLike.toFunLike` `instEquivLike` `sumComm`	—	—
`sumComm_inl` 📖	mathematical	—	`DFunLike.coe` `Diffeomorph` `instTopologicalSpaceSum` `ChartedSpace.sum` `EquivLike.toFunLike` `instEquivLike` `sumComm`	—	—
`sumComm_inr` 📖	mathematical	—	`DFunLike.coe` `Diffeomorph` `instTopologicalSpaceSum` `ChartedSpace.sum` `EquivLike.toFunLike` `instEquivLike` `sumComm`	—	—
`sumComm_symm` 📖	mathematical	—	`symm` `instTopologicalSpaceSum` `ChartedSpace.sum` `sumComm`	—	—
`sumCongr_coe` 📖	mathematical	—	`DFunLike.coe` `Diffeomorph` `instTopologicalSpaceSum` `ChartedSpace.sum` `EquivLike.toFunLike` `instEquivLike` `sumCongr`	—	—
`sumCongr_inl` 📖	mathematical	—	`DFunLike.coe` `Diffeomorph` `instTopologicalSpaceSum` `ChartedSpace.sum` `EquivLike.toFunLike` `instEquivLike` `sumCongr`	—	—
`sumCongr_inr` 📖	mathematical	—	`DFunLike.coe` `Diffeomorph` `instTopologicalSpaceSum` `ChartedSpace.sum` `EquivLike.toFunLike` `instEquivLike` `sumCongr`	—	—
`sumCongr_symm_symm` 📖	mathematical	—	`sumCongr` `symm` `instTopologicalSpaceSum` `ChartedSpace.sum`	—	—
`sumEmpty_apply_inl` 📖	mathematical	—	`DFunLike.coe` `Diffeomorph` `instTopologicalSpaceSum` `ChartedSpace.sum` `EquivLike.toFunLike` `instEquivLike` `sumEmpty`	—	—
`sumEmpty_toEquiv` 📖	mathematical	—	`toEquiv` `instTopologicalSpaceSum` `ChartedSpace.sum` `sumEmpty` `Equiv.sumEmpty`	—	—
`symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.symm_apply_apply`
`symm_image_eq_preimage` 📖	mathematical	—	`Set.image` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike` `symm` `Set.preimage`	—	`image_eq_preimage_symm`
`symm_image_image` 📖	mathematical	—	`Set.image` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.symm_image_image`
`symm_refl` 📖	mathematical	—	`symm` `refl`	—	`ext`
`symm_toEquiv` 📖	mathematical	—	`toEquiv` `symm` `Equiv.symm`	—	—
`symm_toHomeomorph` 📖	mathematical	—	`toHomeomorph` `symm` `Homeomorph.symm`	—	—
`symm_trans'` 📖	mathematical	—	`symm` `trans`	—	—
`symm_trans_self` 📖	mathematical	—	`trans` `symm` `refl`	—	`ext` `apply_symm_apply`
`toEquiv_coe_symm` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toEquiv` `Diffeomorph` `instEquivLike` `symm`	—	—
`toEquiv_inj` 📖	mathematical	—	`toEquiv`	—	`toEquiv_injective`
`toEquiv_injective` 📖	mathematical	—	`Diffeomorph` `Equiv` `toEquiv`	—	—
`toHomeomorph_toEquiv` 📖	mathematical	—	`Homeomorph.toEquiv` `toHomeomorph` `toEquiv`	—	—
`toOpenPartialHomeomorph_mdifferentiable` 📖	mathematical	—	`OpenPartialHomeomorph.MDifferentiable` `Homeomorph.toOpenPartialHomeomorph` `toHomeomorph`	—	`mdifferentiableOn`
`toPartialHomeomorph_mdifferentiable` 📖	mathematical	—	`OpenPartialHomeomorph.MDifferentiable` `Homeomorph.toOpenPartialHomeomorph` `toHomeomorph`	—	`toOpenPartialHomeomorph_mdifferentiable`
`trans_refl` 📖	mathematical	—	`trans` `refl`	—	`ext`
`uniqueDiffOn_image` 📖	mathematical	—	`UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set.image` `DFunLike.coe` `Diffeomorph` `modelWithCornersSelf` `chartedSpaceSelf` `EquivLike.toFunLike` `instEquivLike`	—	`uniqueMDiffOn_image`
`uniqueDiffOn_preimage` 📖	mathematical	—	`UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set.preimage` `DFunLike.coe` `Diffeomorph` `modelWithCornersSelf` `chartedSpaceSelf` `EquivLike.toFunLike` `instEquivLike`	—	`uniqueDiffOn_image` `symm_image_eq_preimage`
`uniqueMDiffOn_image` 📖	mathematical	—	`UniqueMDiffOn` `Set.image` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`uniqueMDiffOn_image_aux` `symm_image_image`
`uniqueMDiffOn_image_aux` 📖	mathematical	`UniqueMDiffOn`	`Set.image` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`image_eq_preimage_symm` `Set.univ_inter` `UniqueMDiffOn.uniqueMDiffOn_preimage` `toOpenPartialHomeomorph_mdifferentiable`
`uniqueMDiffOn_preimage` 📖	mathematical	—	`UniqueMDiffOn` `Set.preimage` `DFunLike.coe` `Diffeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`uniqueMDiffOn_image` `symm_image_eq_preimage`

Manifold

Definitions

Name	Category	Theorems
`«term_≃ₘ[_]_»` 📖	CompOp	—
`«term_≃ₘ^_[_]_»` 📖	CompOp	—
`«term_≃ₘ^_⟮_,_⟯_»` 📖	CompOp	—
`«term_≃ₘ⟮_,_⟯_»` 📖	CompOp	—

ModelWithCorners

Definitions

Name	Category	Theorems
`transContinuousLinearEquiv` 📖	CompOp	15 math math: `ContinuousLinearEquiv.contMDiffAt_transContinuousLinearEquiv_right`, `ContinuousLinearEquiv.contMDiffAt_transContinuousLinearEquiv_left`, `ContinuousLinearEquiv.contMDiffWithinAt_transContinuousLinearEquiv_right`, `ContinuousLinearEquiv.instIsManifoldtransContinuousLinearEquiv`, `coe_extChartAt_transContinuousLinearEquiv_symm`, `ContinuousLinearEquiv.contMDiff_transContinuousLinearEquiv_right`, `ContinuousLinearEquiv.contMDiffWithinAt_transContinuousLinearEquiv_left`, `transContinuousLinearEquiv_range`, `ContinuousLinearEquiv.contMDiff_transContinuousLinearEquiv_left`, `coe_transContinuousLinearEquiv`, `coe_extChartAt_transContinuousLinearEquiv`, `ContinuousLinearEquiv.contMDiffOn_transContinuousLinearEquiv_left`, `coe_transContinuousLinearEquiv_symm`, `ContinuousLinearEquiv.contMDiffOn_transContinuousLinearEquiv_right`, `extChartAt_transContinuousLinearEquiv_target`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_extChartAt_transContinuousLinearEquiv` 📖	mathematical	—	`PartialEquiv.toFun` `extChartAt` `transContinuousLinearEquiv` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike`	—	`RingHomInvPair.ids`
`coe_extChartAt_transContinuousLinearEquiv_symm` 📖	mathematical	—	`PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt` `transContinuousLinearEquiv` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `ContinuousLinearEquiv.symm`	—	`RingHomInvPair.ids`
`coe_transContinuousLinearEquiv` 📖	mathematical	—	`toFun'` `transContinuousLinearEquiv` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike`	—	`RingHomInvPair.ids`
`coe_transContinuousLinearEquiv_symm` 📖	mathematical	—	`PartialEquiv.toFun` `symm` `transContinuousLinearEquiv` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `ContinuousLinearEquiv.symm`	—	`RingHomInvPair.ids`
`extChartAt_transContinuousLinearEquiv_target` 📖	mathematical	—	`PartialEquiv.target` `extChartAt` `transContinuousLinearEquiv` `Set.preimage` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `ContinuousLinearEquiv.symm`	—	`RingHomInvPair.ids` `target_eq` `Set.range_comp` `ContinuousLinearEquiv.image_eq_preimage_symm` `Set.preimage_preimage`
`transContinuousLinearEquiv_range` 📖	mathematical	—	`Set.range` `toFun'` `transContinuousLinearEquiv` `Set.image` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike`	—	`RingHomInvPair.ids` `Set.range_comp`

(root)

Definitions

Name	Category	Theorems
`Diffeomorph` 📖	CompData	52 math math: `Diffeomorph.coe_refl`, `Diffeomorph.contMDiffWithinAt`, `Diffeomorph.toEquiv_injective`, `Diffeomorph.contMDiffOn_comp_diffeomorph_iff`, `Diffeomorph.uniqueMDiffOn_preimage`, `ContinuousLinearEquiv.coe_toDiffeomorph_symm`, `Diffeomorph.apply_symm_apply`, `Diffeomorph.coe_coe`, `Diffeomorph.mdifferentiableOn`, `Diffeomorph.coe_prodCongr`, `Diffeomorph.contMDiff_comp_diffeomorph_iff`, `Diffeomorph.image_eq_preimage_symm`, `Diffeomorph.sumAssoc_coe`, `Diffeomorph.sumCongr_inl`, `Diffeomorph.range_comp`, `Diffeomorph.coeFn_injective`, `Diffeomorph.sumComm_coe`, `Diffeomorph.coe_trans`, `Diffeomorph.isLocalDiffeomorph`, `Diffeomorph.mfderivToContinuousLinearEquiv_coe`, `Diffeomorph.sumComm_inr`, `Diffeomorph.uniqueMDiffOn_image`, `Diffeomorph.contMDiffAt_diffeomorph_comp_iff`, `Diffeomorph.sumCongr_coe`, `Diffeomorph.symm_apply_apply`, `Diffeomorph.coe_prodComm`, `Diffeomorph.contDiff`, `Diffeomorph.symm_image_image`, `Diffeomorph.uniqueDiffOn_image`, `Diffeomorph.sumCongr_inr`, `Diffeomorph.contMDiffOn_diffeomorph_comp_iff`, `Diffeomorph.contMDiffAt_comp_diffeomorph_iff`, `Diffeomorph.mdifferentiable`, `Diffeomorph.sumEmpty_apply_inl`, `Diffeomorph.contMDiffWithinAt_comp_diffeomorph_iff`, `Diffeomorph.coe_toEquiv`, `Diffeomorph.uniqueMDiffOn_image_aux`, `Diffeomorph.continuous`, `Diffeomorph.contMDiffAt`, `Diffeomorph.symm_image_eq_preimage`, `Diffeomorph.uniqueDiffOn_preimage`, `Diffeomorph.instContinuousMapClassSomeENatTop`, `ContinuousLinearEquiv.coe_toDiffeomorph`, `Diffeomorph.contMDiffWithinAt_diffeomorph_comp_iff`, `Diffeomorph.ext_iff`, `Diffeomorph.contMDiff_diffeomorph_comp_iff`, `Diffeomorph.contMDiff`, `Diffeomorph.sumComm_inl`, `Diffeomorph.toEquiv_coe_symm`, `Diffeomorph.image_symm_image`, `Diffeomorph.coe_toHomeomorph_symm`, `Diffeomorph.coe_toHomeomorph`

---

← Back to Index