Immersion

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

Statistics

Metric	Count
Definitions `ImmersionAtProp`, `IsImmersion`, `complement`, `instNormedAddCommGroupComplement`, `instNormedSpaceComplement`, `IsImmersionAt`, `codChart`, `complement`, `domChart`, `equiv`, `instNormedAddCommGroupComplement`, `instNormedSpaceComplement`, `IsImmersionAtOfComplement`, `codChart`, `domChart`, `equiv`, `instNormedAddCommGroupSmallComplement`, `instNormedSpaceSmallComplement`, `smallComplement`, `smallEquiv`, `IsImmersionOfComplement`	21
Theorems `isImmersionAt`, `isImmersionAtOfComplement`, `id`, `isImmersionAt`, `isImmersionOfComplement_complement`, `ofOpen`, `of_opens`, `prodMap`, `codChart_mem_maximalAtlas`, `congr_iff`, `congr_of_eventuallyEq`, `domChart_mem_maximalAtlas`, `isImmersionAtOfComplement_complement`, `map_target_subset_target`, `mem_codChart_source`, `mem_domChart_source`, `mk_of_charts`, `mk_of_continuousAt`, `ofOpen`, `of_opens`, `prodMap`, `property`, `source_subset_preimage_source`, `target_subset_preimage_target`, `writtenInCharts`, `codChart_mem_maximalAtlas`, `congr_F`, `congr_iff_of_eventuallyEq`, `congr_of_eventuallyEq`, `domChart_mem_maximalAtlas`, `isImmersionAt`, `map_target_subset_target`, `mem_codChart_source`, `mem_domChart_source`, `mk_of_charts`, `mk_of_continuousAt`, `ofOpen`, `of_opens`, `prodMap`, `property`, `small`, `source_subset_preimage_source`, `target_subset_preimage_target`, `trans_F`, `writtenInCharts`, `IsImmersionAtOfComplement_def`, `IsImmersionAt_def`, `congr_F`, `id`, `isImmersion`, `isImmersionAt`, `ofOpen`, `of_opens`, `prodMap`, `trans_F`, `isLocalSourceTargetProperty_immersionAtProp`	56
Total	77

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isImmersionAt` 📖	mathematical	—	`IsOpen` `setOf` `Manifold.IsImmersionAt`	—	`isOpen_iff_forall_mem_open` `Manifold.IsImmersionAtOfComplement.isImmersionAt` `isImmersionAtOfComplement` `Manifold.IsImmersionAt.isImmersionAtOfComplement_complement`
`isImmersionAtOfComplement` 📖	mathematical	—	`IsOpen` `setOf` `Manifold.IsImmersionAtOfComplement`	—	`Manifold.IsImmersionAtOfComplement_def` `liftSourceTargetPropertyAt`

Manifold

Definitions

Name	Category	Theorems
`ImmersionAtProp` 📖	MathDef	4 math math: `IsImmersionAtOfComplement_def`, `IsImmersionAt.property`, `isLocalSourceTargetProperty_immersionAtProp`, `IsImmersionAtOfComplement.property`
`IsImmersion` 📖	MathDef	6 math math: `IsImmersion.of_opens`, `IsImmersion.id`, `IsImmersion.ofOpen`, `IsSmoothEmbedding.isImmersion`, `IsImmersionOfComplement.isImmersion`, `isSmoothEmbedding_iff`
`IsImmersionAt` 📖	MathDef	9 math math: `IsImmersionAt_def`, `IsImmersionAtOfComplement.isImmersionAt`, `IsImmersionAt.of_opens`, `IsImmersion.isImmersionAt`, `IsOpen.isImmersionAt`, `IsImmersionAt.mk_of_continuousAt`, `IsImmersionAt.ofOpen`, `IsImmersionAt.mk_of_charts`, `IsImmersionAt.congr_iff`
`IsImmersionAtOfComplement` 📖	MathDef	11 math math: `IsImmersionAt_def`, `IsImmersionAtOfComplement_def`, `IsImmersionAtOfComplement.mk_of_charts`, `IsImmersionAtOfComplement.ofOpen`, `IsImmersionOfComplement.isImmersionAt`, `IsImmersionAtOfComplement.congr_F`, `IsImmersionAt.isImmersionAtOfComplement_complement`, `IsImmersionAtOfComplement.mk_of_continuousAt`, `IsImmersionAtOfComplement.of_opens`, `IsImmersionAtOfComplement.congr_iff_of_eventuallyEq`, `IsOpen.isImmersionAtOfComplement`
`IsImmersionOfComplement` 📖	MathDef	5 math math: `IsImmersionOfComplement.ofOpen`, `IsImmersion.isImmersionOfComplement_complement`, `IsImmersionOfComplement.id`, `IsImmersionOfComplement.of_opens`, `IsImmersionOfComplement.congr_F`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`IsImmersionAtOfComplement_def` 📖	mathematical	—	`IsImmersionAtOfComplement` `LiftSourceTargetPropertyAt` `ImmersionAtProp`	—	—
`IsImmersionAt_def` 📖	mathematical	—	`IsImmersionAt` `NormedAddCommGroup` `NormedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `IsImmersionAtOfComplement`	—	—
`isLocalSourceTargetProperty_immersionAtProp` 📖	mathematical	—	`IsLocalSourceTargetProperty` `ImmersionAtProp`	—	`Set.EqOn.mono` `ModelWithCorners.target_eq` `Set.EqOn.trans` `Set.instReflSubset`

Manifold.IsImmersion

Definitions

Name	Category	Theorems
`complement` 📖	CompOp	1 math math: `isImmersionOfComplement_complement`
`instNormedAddCommGroupComplement` 📖	CompOp	1 math math: `isImmersionOfComplement_complement`
`instNormedSpaceComplement` 📖	CompOp	1 math math: `isImmersionOfComplement_complement`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`id` 📖	mathematical	—	`Manifold.IsImmersion`	—	`Manifold.IsImmersionOfComplement.id`
`isImmersionAt` 📖	mathematical	`Manifold.IsImmersion`	`Manifold.IsImmersionAt`	—	`Manifold.IsImmersionAt_def` `isImmersionOfComplement_complement`
`isImmersionOfComplement_complement` 📖	mathematical	`Manifold.IsImmersion`	`Manifold.IsImmersionOfComplement` `complement` `instNormedAddCommGroupComplement` `instNormedSpaceComplement`	—	—
`ofOpen` 📖	mathematical	—	`Manifold.IsImmersion` `TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `instTopologicalSpaceSubtype` `TopologicalSpace.Opens.instChartedSpace`	—	`of_opens`
`of_opens` 📖	mathematical	—	`Manifold.IsImmersion` `TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `instTopologicalSpaceSubtype` `TopologicalSpace.Opens.instChartedSpace`	—	`Manifold.IsImmersionOfComplement.of_opens`
`prodMap` 📖	mathematical	`Manifold.IsImmersion`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`Manifold.IsImmersionOfComplement.isImmersion` `Manifold.IsImmersionOfComplement.prodMap` `isImmersionOfComplement_complement`

Manifold.IsImmersionAt

Definitions

Name	Category	Theorems
`codChart` 📖	CompOp	6 math math: `map_target_subset_target`, `writtenInCharts`, `mem_codChart_source`, `codChart_mem_maximalAtlas`, `source_subset_preimage_source`, `target_subset_preimage_target`
`complement` 📖	CompOp	5 math math: `map_target_subset_target`, `writtenInCharts`, `property`, `isImmersionAtOfComplement_complement`, `target_subset_preimage_target`
`domChart` 📖	CompOp	6 math math: `map_target_subset_target`, `mem_domChart_source`, `writtenInCharts`, `source_subset_preimage_source`, `target_subset_preimage_target`, `domChart_mem_maximalAtlas`
`equiv` 📖	CompOp	3 math math: `map_target_subset_target`, `writtenInCharts`, `target_subset_preimage_target`
`instNormedAddCommGroupComplement` 📖	CompOp	5 math math: `map_target_subset_target`, `writtenInCharts`, `property`, `isImmersionAtOfComplement_complement`, `target_subset_preimage_target`
`instNormedSpaceComplement` 📖	CompOp	5 math math: `map_target_subset_target`, `writtenInCharts`, `property`, `isImmersionAtOfComplement_complement`, `target_subset_preimage_target`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`codChart_mem_maximalAtlas` 📖	mathematical	`Manifold.IsImmersionAt`	`OpenPartialHomeomorph` `Set` `Set.instMembership` `IsManifold.maximalAtlas` `codChart`	—	`Manifold.IsImmersionAtOfComplement.codChart_mem_maximalAtlas` `isImmersionAtOfComplement_complement`
`congr_iff` 📖	mathematical	`Filter.EventuallyEq` `nhds`	`Manifold.IsImmersionAt`	—	`congr_of_eventuallyEq` `Filter.EventuallyEq.symm`
`congr_of_eventuallyEq` 📖	—	`Manifold.IsImmersionAt` `Filter.EventuallyEq` `nhds`	—	—	`Manifold.IsImmersionAt_def` `Manifold.IsImmersionAtOfComplement.congr_of_eventuallyEq` `isImmersionAtOfComplement_complement`
`domChart_mem_maximalAtlas` 📖	mathematical	`Manifold.IsImmersionAt`	`OpenPartialHomeomorph` `Set` `Set.instMembership` `IsManifold.maximalAtlas` `domChart`	—	`Manifold.IsImmersionAtOfComplement.domChart_mem_maximalAtlas` `isImmersionAtOfComplement_complement`
`isImmersionAtOfComplement_complement` 📖	mathematical	`Manifold.IsImmersionAt`	`Manifold.IsImmersionAtOfComplement` `complement` `instNormedAddCommGroupComplement` `instNormedSpaceComplement`	—	`Manifold.IsImmersionAt_def`
`map_target_subset_target` 📖	mathematical	`Manifold.IsImmersionAt`	`Set` `Set.instHasSubset` `Set.image` `complement` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instNormedAddCommGroupComplement` `Prod.instAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Prod.instModule` `NormedSpace.toModule` `instNormedSpaceComplement` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `equiv` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `PartialEquiv.target` `OpenPartialHomeomorph.extend` `domChart` `codChart`	—	`Manifold.IsImmersionAtOfComplement.map_target_subset_target` `isImmersionAtOfComplement_complement`
`mem_codChart_source` 📖	mathematical	`Manifold.IsImmersionAt`	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `codChart`	—	`Manifold.IsImmersionAtOfComplement.mem_codChart_source` `isImmersionAtOfComplement_complement`
`mem_domChart_source` 📖	mathematical	`Manifold.IsImmersionAt`	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `domChart`	—	`Manifold.IsImmersionAtOfComplement.mem_domChart_source` `isImmersionAtOfComplement_complement`
`mk_of_charts` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `OpenPartialHomeomorph` `IsManifold.maximalAtlas` `Set.instHasSubset` `Set.preimage` `Set.EqOn` `PartialEquiv.toFun` `OpenPartialHomeomorph.extend` `PartialEquiv.symm` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Prod.instModule` `NormedSpace.toModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `PartialEquiv.target`	`Manifold.IsImmersionAt`	—	`RingHomInvPair.ids` `Manifold.IsImmersionAt_def` `Manifold.IsImmersionAtOfComplement.mk_of_charts` `Manifold.IsImmersionAtOfComplement.congr_F`
`mk_of_continuousAt` 📖	mathematical	`ContinuousAt` `Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `OpenPartialHomeomorph` `IsManifold.maximalAtlas` `Set.EqOn` `PartialEquiv.toFun` `OpenPartialHomeomorph.extend` `PartialEquiv.symm` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Prod.instModule` `NormedSpace.toModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `PartialEquiv.target`	`Manifold.IsImmersionAt`	—	`RingHomInvPair.ids` `Manifold.IsImmersionAt_def` `Manifold.IsImmersionAtOfComplement.mk_of_continuousAt` `Manifold.IsImmersionAtOfComplement.congr_F`
`ofOpen` 📖	mathematical	`TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	`Manifold.IsImmersionAt` `instTopologicalSpaceSubtype` `TopologicalSpace.Opens.instChartedSpace`	—	`of_opens`
`of_opens` 📖	mathematical	`TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	`Manifold.IsImmersionAt` `instTopologicalSpaceSubtype` `TopologicalSpace.Opens.instChartedSpace`	—	`Manifold.IsImmersionAt_def` `Manifold.IsImmersionAtOfComplement.of_opens`
`prodMap` 📖	mathematical	`Manifold.IsImmersionAt`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`Manifold.IsImmersionAtOfComplement.isImmersionAt` `Manifold.IsImmersionAtOfComplement.prodMap` `isImmersionAtOfComplement_complement`
`property` 📖	mathematical	`Manifold.IsImmersionAt`	`Manifold.LiftSourceTargetPropertyAt` `Manifold.ImmersionAtProp` `complement` `instNormedAddCommGroupComplement` `instNormedSpaceComplement`	—	`Manifold.IsImmersionAtOfComplement.property` `isImmersionAtOfComplement_complement`
`source_subset_preimage_source` 📖	mathematical	`Manifold.IsImmersionAt`	`Set` `Set.instHasSubset` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `domChart` `Set.preimage` `codChart`	—	`Manifold.IsImmersionAtOfComplement.source_subset_preimage_source` `isImmersionAtOfComplement_complement`
`target_subset_preimage_target` 📖	mathematical	`Manifold.IsImmersionAt`	`Set` `Set.instHasSubset` `PartialEquiv.target` `OpenPartialHomeomorph.extend` `domChart` `Set.preimage` `complement` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instNormedAddCommGroupComplement` `Prod.instAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Prod.instModule` `NormedSpace.toModule` `instNormedSpaceComplement` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `equiv` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `codChart`	—	`map_target_subset_target` `RingHomInvPair.ids` `Set.mem_image_of_mem`
`writtenInCharts` 📖	mathematical	`Manifold.IsImmersionAt`	`Set.EqOn` `PartialEquiv.toFun` `OpenPartialHomeomorph.extend` `codChart` `PartialEquiv.symm` `domChart` `complement` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instNormedAddCommGroupComplement` `Prod.instAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Prod.instModule` `NormedSpace.toModule` `instNormedSpaceComplement` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `equiv` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `PartialEquiv.target`	—	`Manifold.IsImmersionAtOfComplement.writtenInCharts` `isImmersionAtOfComplement_complement`

Manifold.IsImmersionAtOfComplement

Definitions

Name	Category	Theorems
`codChart` 📖	CompOp	6 math math: `target_subset_preimage_target`, `map_target_subset_target`, `source_subset_preimage_source`, `mem_codChart_source`, `writtenInCharts`, `codChart_mem_maximalAtlas`
`domChart` 📖	CompOp	6 math math: `target_subset_preimage_target`, `map_target_subset_target`, `mem_domChart_source`, `source_subset_preimage_source`, `domChart_mem_maximalAtlas`, `writtenInCharts`
`equiv` 📖	CompOp	3 math math: `target_subset_preimage_target`, `map_target_subset_target`, `writtenInCharts`
`instNormedAddCommGroupSmallComplement` 📖	CompOp	—
`instNormedSpaceSmallComplement` 📖	CompOp	—
`smallComplement` 📖	CompOp	—
`smallEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`codChart_mem_maximalAtlas` 📖	mathematical	`Manifold.IsImmersionAtOfComplement`	`OpenPartialHomeomorph` `Set` `Set.instMembership` `IsManifold.maximalAtlas` `codChart`	—	`Manifold.LiftSourceTargetPropertyAt.codChart_mem_maximalAtlas` `Manifold.IsImmersionAtOfComplement_def`
`congr_F` 📖	mathematical	—	`Manifold.IsImmersionAtOfComplement`	—	`RingHomInvPair.ids` `trans_F`
`congr_iff_of_eventuallyEq` 📖	mathematical	`Filter.EventuallyEq` `nhds`	`Manifold.IsImmersionAtOfComplement`	—	`Manifold.IsImmersionAtOfComplement_def` `Manifold.LiftSourceTargetPropertyAt.congr_iff_of_eventuallyEq` `Manifold.isLocalSourceTargetProperty_immersionAtProp`
`congr_of_eventuallyEq` 📖	—	`Manifold.IsImmersionAtOfComplement` `Filter.EventuallyEq` `nhds`	—	—	`Manifold.IsImmersionAtOfComplement_def` `Manifold.LiftSourceTargetPropertyAt.congr_of_eventuallyEq` `Manifold.isLocalSourceTargetProperty_immersionAtProp` `property`
`domChart_mem_maximalAtlas` 📖	mathematical	`Manifold.IsImmersionAtOfComplement`	`OpenPartialHomeomorph` `Set` `Set.instMembership` `IsManifold.maximalAtlas` `domChart`	—	`Manifold.LiftSourceTargetPropertyAt.domChart_mem_maximalAtlas` `Manifold.IsImmersionAtOfComplement_def`
`isImmersionAt` 📖	mathematical	`Manifold.IsImmersionAtOfComplement`	`Manifold.IsImmersionAt`	—	`Manifold.IsImmersionAt_def` `congr_F`
`map_target_subset_target` 📖	mathematical	`Manifold.IsImmersionAtOfComplement`	`Set` `Set.instHasSubset` `Set.image` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Prod.instModule` `NormedSpace.toModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `equiv` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `PartialEquiv.target` `OpenPartialHomeomorph.extend` `domChart` `codChart`	—	`RingHomInvPair.ids` `Set.EqOn.image_eq` `writtenInCharts` `Set.image_comp` `PartialEquiv.symm_image_target_eq_source` `OpenPartialHomeomorph.extend_source` `PartialEquiv.image_source_eq_target` `source_subset_preimage_source` `Mathlib.Tactic.GCongr.rel_imp_rel` `Set.instIsTransSubset` `Set.image_mono` `subset_refl` `Set.instReflSubset`
`mem_codChart_source` 📖	mathematical	`Manifold.IsImmersionAtOfComplement`	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `codChart`	—	`Manifold.LiftSourceTargetPropertyAt.mem_codChart_source` `Manifold.IsImmersionAtOfComplement_def`
`mem_domChart_source` 📖	mathematical	`Manifold.IsImmersionAtOfComplement`	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `domChart`	—	`Manifold.LiftSourceTargetPropertyAt.mem_domChart_source` `Manifold.IsImmersionAtOfComplement_def`
`mk_of_charts` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `OpenPartialHomeomorph` `IsManifold.maximalAtlas` `Set.instHasSubset` `Set.preimage` `Set.EqOn` `PartialEquiv.toFun` `OpenPartialHomeomorph.extend` `PartialEquiv.symm` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Prod.instModule` `NormedSpace.toModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `PartialEquiv.target`	`Manifold.IsImmersionAtOfComplement`	—	`RingHomInvPair.ids` `Manifold.IsImmersionAtOfComplement_def`
`mk_of_continuousAt` 📖	mathematical	`ContinuousAt` `Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `OpenPartialHomeomorph` `IsManifold.maximalAtlas` `Set.EqOn` `PartialEquiv.toFun` `OpenPartialHomeomorph.extend` `PartialEquiv.symm` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Prod.instModule` `NormedSpace.toModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `PartialEquiv.target`	`Manifold.IsImmersionAtOfComplement`	—	`RingHomInvPair.ids` `Manifold.IsImmersionAtOfComplement_def` `Manifold.LiftSourceTargetPropertyAt.mk_of_continuousAt` `Manifold.isLocalSourceTargetProperty_immersionAtProp`
`ofOpen` 📖	mathematical	—	`Manifold.IsImmersionAtOfComplement` `PUnit.normedAddCommGroup` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `PUnit.normedCommRing` `PUnit.normedAlgebra` `TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `instTopologicalSpaceSubtype` `TopologicalSpace.Opens.instChartedSpace`	—	`of_opens`
`of_opens` 📖	mathematical	—	`Manifold.IsImmersionAtOfComplement` `PUnit.normedAddCommGroup` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `PUnit.normedCommRing` `PUnit.normedAlgebra` `TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `instTopologicalSpaceSubtype` `TopologicalSpace.Opens.instChartedSpace`	—	`mk_of_continuousAt` `Continuous.continuousAt` `continuous_subtype_val` `mem_chart_source` `IsManifold.chart_mem_maximalAtlas` `TopologicalSpace.Opens.instIsManifoldSubtypeMem` `OpenPartialHomeomorph.right_inv` `ModelWithCorners.target_eq` `ModelWithCorners.right_inv` `RingHomInvPair.ids`
`prodMap` 📖	mathematical	`Manifold.IsImmersionAtOfComplement`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`Manifold.IsImmersionAtOfComplement_def` `Manifold.LiftSourceTargetPropertyAt.prodMap` `property` `RingHomInvPair.ids` `RingHomCompTriple.ids` `OpenPartialHomeomorph.extend_prod` `PartialEquiv.prod_target` `Set.eqOn_prod_iff` `PartialEquiv.prod_symm`
`property` 📖	mathematical	`Manifold.IsImmersionAtOfComplement`	`Manifold.LiftSourceTargetPropertyAt` `Manifold.ImmersionAtProp`	—	`Manifold.IsImmersionAtOfComplement_def`
`small` 📖	mathematical	`Manifold.IsImmersionAtOfComplement`	`Small`	—	`small_of_injective` `UnivLE.small` `UnivLE.self` `RingHomInvPair.ids` `ContinuousLinearEquiv.injective` `Prod.mk_right_injective`
`source_subset_preimage_source` 📖	mathematical	`Manifold.IsImmersionAtOfComplement`	`Set` `Set.instHasSubset` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `domChart` `Set.preimage` `codChart`	—	`Manifold.LiftSourceTargetPropertyAt.source_subset_preimage_source` `Manifold.IsImmersionAtOfComplement_def`
`target_subset_preimage_target` 📖	mathematical	`Manifold.IsImmersionAtOfComplement`	`Set` `Set.instHasSubset` `PartialEquiv.target` `OpenPartialHomeomorph.extend` `domChart` `Set.preimage` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Prod.instModule` `NormedSpace.toModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `equiv` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `codChart`	—	`map_target_subset_target` `RingHomInvPair.ids` `Set.mem_image_of_mem`
`trans_F` 📖	—	`Manifold.IsImmersionAtOfComplement`	—	—	`RingHomInvPair.ids` `Manifold.IsImmersionAtOfComplement_def` `mem_domChart_source` `mem_codChart_source` `domChart_mem_maximalAtlas` `codChart_mem_maximalAtlas` `source_subset_preimage_source` `RingHomCompTriple.ids` `Set.EqOn.trans` `writtenInCharts` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousSemilinearEquivClass.continuousSemilinearMapClass` `ContinuousLinearEquiv.continuousSemilinearEquivClass`
`writtenInCharts` 📖	mathematical	`Manifold.IsImmersionAtOfComplement`	`Set.EqOn` `PartialEquiv.toFun` `OpenPartialHomeomorph.extend` `codChart` `PartialEquiv.symm` `domChart` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Prod.instModule` `NormedSpace.toModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `equiv` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `PartialEquiv.target`	—	`Manifold.IsImmersionAtOfComplement_def` `Manifold.LiftSourceTargetPropertyAt.property`

Manifold.IsImmersionOfComplement

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_F` 📖	mathematical	—	`Manifold.IsImmersionOfComplement`	—	`RingHomInvPair.ids` `trans_F`
`id` 📖	mathematical	—	`Manifold.IsImmersionOfComplement` `PUnit.normedAddCommGroup` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `PUnit.normedCommRing` `PUnit.normedAlgebra`	—	`Manifold.IsImmersionAtOfComplement.mk_of_continuousAt` `continuousAt_id` `mem_chart_source` `IsManifold.chart_mem_maximalAtlas` `OpenPartialHomeomorph.right_inv` `ModelWithCorners.target_eq` `ModelWithCorners.right_inv` `RingHomInvPair.ids` `CompTriple.comp_eq` `CompTriple.instId_comp` `CompTriple.instIsIdId`
`isImmersion` 📖	mathematical	`Manifold.IsImmersionOfComplement`	`Manifold.IsImmersion`	—	`Manifold.IsImmersion.eq_1` `IsEmpty.false` `congr_F`
`isImmersionAt` 📖	mathematical	`Manifold.IsImmersionOfComplement`	`Manifold.IsImmersionAtOfComplement`	—	—
`ofOpen` 📖	mathematical	—	`Manifold.IsImmersionOfComplement` `PUnit.normedAddCommGroup` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `PUnit.normedCommRing` `PUnit.normedAlgebra` `TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `instTopologicalSpaceSubtype` `TopologicalSpace.Opens.instChartedSpace`	—	`of_opens`
`of_opens` 📖	mathematical	—	`Manifold.IsImmersionOfComplement` `PUnit.normedAddCommGroup` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `PUnit.normedCommRing` `PUnit.normedAlgebra` `TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `instTopologicalSpaceSubtype` `TopologicalSpace.Opens.instChartedSpace`	—	`Manifold.IsImmersionAtOfComplement.of_opens`
`prodMap` 📖	mathematical	`Manifold.IsImmersionOfComplement`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace`	—	`Manifold.IsImmersionAtOfComplement.prodMap`
`trans_F` 📖	—	`Manifold.IsImmersionOfComplement`	—	—	`RingHomInvPair.ids` `Manifold.IsImmersionAtOfComplement.trans_F`

---

← Back to Index