Pullback

📁 Source: Mathlib/Geometry/Manifold/VectorField/Pullback.lean

Statistics

Metric	Count
Definitions `Pullback`, `Pullback`, `mpullback`, `mpullbackWithin`	4
Theorems `mpullback_vectorField`, `mpullback_vectorField_preimage`, `mpullbackWithin_vectorField_inter`, `mpullback_vectorField_preimage`, `mpullbackWithin_vectorField`, `mpullbackWithin_vectorField'`, `mpullbackWithin_vectorField_inter`, `mpullbackWithin_vectorField_inter_of_eq`, `mpullbackWithin_vectorField_of_eq`, `mpullbackWithin_vectorField_of_eq'`, `mpullbackWithin_vectorField_of_mem`, `mpullbackWithin_vectorField_of_mem_of_eq`, `mpullback_vectorField_of_mem_nhdsWithin`, `mpullback_vectorField_of_mem_nhdsWithin_of_eq`, `mpullback_vectorField_preimage`, `mpullback_vectorField_preimage_of_eq`, `mpullback_vectorField`, `mpullback_vectorField`, `mpullbackWithin_vectorField_inter`, `mpullback_vectorField_preimage`, `mpullbackWithin_vectorField_inter`, `mpullbackWithin_vectorField_inter_of_eq`, `mpullback_vectorField_preimage`, `mpullback_vectorField_preimage_of_eq`, `contMDiffWithinAt_mpullbackWithin_extChartAt_symm`, `eventuallyEq_mpullback_mpullbackWithin_extChartAt`, `eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm`, `mpullbackWithin_add`, `mpullbackWithin_add_apply`, `mpullbackWithin_apply`, `mpullbackWithin_comp_of_left`, `mpullbackWithin_comp_of_right`, `mpullbackWithin_eq_pullbackWithin`, `mpullbackWithin_id`, `mpullbackWithin_neg`, `mpullbackWithin_neg_apply`, `mpullbackWithin_smul`, `mpullbackWithin_smul_apply`, `mpullbackWithin_univ`, `mpullbackWithin_zero`, `mpullback_add`, `mpullback_add_apply`, `mpullback_apply`, `mpullback_eq_pullback`, `mpullback_id`, `mpullback_neg`, `mpullback_neg_apply`, `mpullback_smul`, `mpullback_smul_apply`, `mpullback_zero`, `instIsManifoldMinSmoothnessOfNatWithTopENat`, `instIsManifoldMinSmoothnessOfNatWithTopENat_1`, `instIsManifoldOfNatWithTopENatOfMinSmoothness`, `instIsManifoldOfNatWithTopENatOfMinSmoothness_1`	54
Total	58

Bundle

Definitions

Name	Category	Theorems
`Pullback` 📖	CompOp	20 math math: `Trivialization.pullback_linear`, `Trivialization.pullback_source`, `Pullback.lift_mk`, `Pullback.continuous_lift`, `ContMDiffVectorBundle.pullback`, `Trivialization.pullback_target`, `instNonemptyPullback`, `FiberBundle.pullback_trivializationAt'`, `FiberBundle.pullback_trivializationAtlas'`, `pullbackTopology_def`, `Pullback.continuous_proj`, `Trivialization.pullback_apply`, `Pullback.continuous_totalSpaceMk`, `Trivialization.pullback_symm_apply_snd`, `Trivialization.pullback_baseSet`, `inducing_pullbackTotalSpaceEmbedding`, `Trivialization.pullback_symm_apply_proj`, `Pullback.lift_snd`, `VectorBundle.pullback`, `Pullback.lift_proj`

ContMDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mpullback_vectorField` 📖	mathematical	`ContMDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderiv` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`VectorField.mpullback`	—	`ContMDiffAt.mpullback_vectorField_preimage`

ContMDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mpullback_vectorField_preimage` 📖	mathematical	`ContMDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderiv` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`VectorField.mpullback`	—	`ContMDiffWithinAt.mpullback_vectorField_preimage`

ContMDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mpullbackWithin_vectorField_inter` 📖	mathematical	`ContMDiffOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderivWithin` `UniqueMDiffOn` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`VectorField.mpullbackWithin` `Set` `Set.instInter` `Set.preimage`	—	`ContMDiffWithinAt.mpullbackWithin_vectorField_inter`
`mpullback_vectorField_preimage` 📖	mathematical	`ContMDiffOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContMDiff` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderiv` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`VectorField.mpullback` `Set.preimage`	—	`ContMDiffWithinAt.mpullback_vectorField_preimage`

ContMDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mpullbackWithin_vectorField` 📖	mathematical	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderivWithin` `Set` `Set.instMembership` `UniqueMDiffOn` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Set.MapsTo`	`VectorField.mpullbackWithin`	—	`mpullbackWithin_vectorField_of_mem` `Set.MapsTo.preimage_mem_nhdsWithin`
`mpullbackWithin_vectorField'` 📖	mathematical	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderivWithin` `Set` `Set.instMembership` `UniqueMDiffOn` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Filter` `Filter.instMembership` `nhdsWithin` `Set.preimage` `Set.instHasSubset`	`VectorField.mpullbackWithin`	—	`le_trans` `WithTop.canonicallyOrderedAdd` `MDifferentiableWithinAt.mfderivWithin_mono` `mdifferentiableWithinAt` `ne_of_gt` `lt_of_lt_of_le` `Mathlib.Meta.Positivity.pos_of_isNat` `WithTop.instIsOrderedRing` `WithTop.nontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `congr_of_eventuallyEq_of_mem` `mpullbackWithin_vectorField_of_mem` `mono` `contMDiffWithinAt_iff_contMDiffWithinAt_nhdsWithin` `of_le` `Filter.mp_mem` `nhdsWithin_mono` `Set.insert_eq_of_mem` `self_mem_nhdsWithin` `Filter.univ_mem'` `one_ne_zero` `NeZero.charZero_one` `WithTop.charZero`
`mpullbackWithin_vectorField_inter` 📖	mathematical	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderivWithin` `Set` `Set.instMembership` `UniqueMDiffOn` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`VectorField.mpullbackWithin` `Set.instInter` `Set.preimage`	—	`comp` `mono` `of_le` `le_trans` `le_self_add` `WithTop.canonicallyOrderedAdd` `Set.inter_subset_left` `Set.MapsTo.mono_left` `Set.mapsTo_preimage` `Set.inter_subset_right` `RingHomIsometric.ids` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `TangentSpace.vectorBundle` `mfderivWithin_const` `ContMDiffAt.comp_contMDiffWithinAt` `ContDiffAt.contMDiffAt` `ContinuousLinearMap.IsInvertible.contDiffAt_map_inverse` `RingHomCompTriple.right_ids` `RingHomInvPair.ids` `trivialization_linear` `instMemTrivializationAtlasTrivializationAt` `FiberBundle.mem_baseSet_trivializationAt'` `RingHomCompTriple.ids` `ContinuousLinearMap.inCoordinates_eq` `ContinuousLinearMap.IsInvertible.comp` `ContinuousLinearMap.isInvertible_equiv` `congr_of_eventuallyEq_of_mem` `nhdsWithin_le_nhds` `IsOpen.mem_nhds` `Trivialization.open_baseSet` `ContinuousWithinAt.preimage_mem_nhdsWithin` `continuousWithinAt` `Filter.mp_mem` `Filter.univ_mem'` `ContinuousLinearMap.inverse_equiv_comp` `ContinuousLinearMap.comp.congr_simp` `ContinuousLinearMap.inverse_comp_equiv` `clm_apply_of_inCoordinates` `contMDiffWithinAt_id`
`mpullbackWithin_vectorField_inter_of_eq` 📖	mathematical	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderivWithin` `Set` `Set.instMembership` `UniqueMDiffOn` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`VectorField.mpullbackWithin` `Set.instInter` `Set.preimage`	—	`mpullbackWithin_vectorField_inter`
`mpullbackWithin_vectorField_of_eq` 📖	mathematical	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderivWithin` `Set` `Set.instMembership` `UniqueMDiffOn` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Set.MapsTo`	`VectorField.mpullbackWithin`	—	`mpullbackWithin_vectorField`
`mpullbackWithin_vectorField_of_eq'` 📖	mathematical	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderivWithin` `Set` `Set.instMembership` `UniqueMDiffOn` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Filter` `Filter.instMembership` `nhdsWithin` `Set.preimage` `Set.instHasSubset`	`VectorField.mpullbackWithin`	—	`mpullbackWithin_vectorField'`
`mpullbackWithin_vectorField_of_mem` 📖	mathematical	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderivWithin` `Set` `Set.instMembership` `UniqueMDiffOn` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Filter` `Filter.instMembership` `nhdsWithin` `Set.preimage`	`VectorField.mpullbackWithin`	—	`mono_of_mem_nhdsWithin` `mpullbackWithin_vectorField_inter` `Filter.inter_mem` `self_mem_nhdsWithin`
`mpullbackWithin_vectorField_of_mem_of_eq` 📖	mathematical	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderivWithin` `Set` `Set.instMembership` `UniqueMDiffOn` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Filter` `Filter.instMembership` `nhdsWithin` `Set.preimage`	`VectorField.mpullbackWithin`	—	`mpullbackWithin_vectorField_of_mem`
`mpullback_vectorField_of_mem_nhdsWithin` 📖	mathematical	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContMDiffAt` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderiv` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.preimage`	`VectorField.mpullback`	—	`mono_of_mem_nhdsWithin` `mpullback_vectorField_preimage`
`mpullback_vectorField_of_mem_nhdsWithin_of_eq` 📖	mathematical	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContMDiffAt` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderiv` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.preimage`	`VectorField.mpullback`	—	`mpullback_vectorField_of_mem_nhdsWithin`
`mpullback_vectorField_preimage` 📖	mathematical	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContMDiffAt` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderiv` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`VectorField.mpullback` `Set.preimage`	—	`VectorField.mpullbackWithin_univ` `Set.univ_inter` `mpullbackWithin_vectorField_inter` `Set.mem_univ` `uniqueMDiffOn_univ`
`mpullback_vectorField_preimage_of_eq` 📖	mathematical	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContMDiffAt` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderiv` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`VectorField.mpullback` `Set.preimage`	—	`mpullback_vectorField_preimage`

Function

Definitions

Name	Category	Theorems
`Pullback` 📖	CompOp	15 math math: `IsSeparatedMap.pullback`, `injective_toPullbackDiag`, `isLocallyInjective_iff_isOpen_diagonal`, `isSeparatedMap_iff_isClosedEmbedding`, `isSeparatedMap_iff_isClosedMap`, `isLocallyInjective_iff_isOpenMap`, `Topology.IsEmbedding.toPullbackDiag`, `range_toPullbackDiag`, `pullback_comm_sq`, `IsLocallyInjective_iff_isOpenEmbedding`, `preimage_map_fst_pullbackDiagonal`, `image_toPullbackDiag`, `Injective.preimage_pullbackDiagonal`, `isSeparatedMap_iff_isClosed_diagonal`, `Continuous.mapPullback`

MDifferentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mpullback_vectorField` 📖	mathematical	`MDifferentiable` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContMDiff` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderiv` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat`	`VectorField.mpullback`	—	`Nat.instAtLeastTwoHAddOfNat` `IsManifold.instOfNatWithTopENat_1` `MDifferentiableAt.mpullback_vectorField`

MDifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mpullback_vectorField` 📖	mathematical	`MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContMDiffAt` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderiv` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat`	`VectorField.mpullback`	—	`Nat.instAtLeastTwoHAddOfNat` `IsManifold.instOfNatWithTopENat_1` `MDifferentiableWithinAt.mpullback_vectorField_preimage`

MDifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mpullbackWithin_vectorField_inter` 📖	mathematical	`MDifferentiableOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContMDiffOn` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderivWithin` `UniqueMDiffOn` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat`	`VectorField.mpullbackWithin` `Set` `Set.instInter` `Set.preimage`	—	`Nat.instAtLeastTwoHAddOfNat` `IsManifold.instOfNatWithTopENat_1` `MDifferentiableWithinAt.mpullbackWithin_vectorField_inter`
`mpullback_vectorField_preimage` 📖	mathematical	`MDifferentiableOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContMDiff` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderiv` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat`	`VectorField.mpullback` `Set.preimage`	—	`Nat.instAtLeastTwoHAddOfNat` `IsManifold.instOfNatWithTopENat_1` `MDifferentiableWithinAt.mpullback_vectorField_preimage`

MDifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mpullbackWithin_vectorField_inter` 📖	mathematical	`MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContMDiffWithinAt` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderivWithin` `Set` `Set.instMembership` `UniqueMDiffOn` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat`	`VectorField.mpullbackWithin` `Set.instInter` `Set.preimage`	—	`Nat.instAtLeastTwoHAddOfNat` `IsManifold.instOfNatWithTopENat_1` `comp` `mono` `Set.inter_subset_left` `ContMDiffWithinAt.mdifferentiableWithinAt` `ne_of_gt` `lt_of_lt_of_le` `Mathlib.Meta.Positivity.pos_of_isNat` `WithTop.instIsOrderedRing` `WithTop.nontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Set.MapsTo.mono_left` `Set.mapsTo_preimage` `Set.inter_subset_right` `RingHomIsometric.ids` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `TangentSpace.vectorBundle` `ContMDiffWithinAt.mfderivWithin_const` `ContMDiffWithinAt.of_le` `le_rfl` `one_ne_zero` `NeZero.charZero_one` `WithTop.charZero` `MDifferentiableAt.comp_mdifferentiableWithinAt` `ContMDiffAt.mdifferentiableAt` `ContDiffAt.contMDiffAt` `ContinuousLinearMap.IsInvertible.contDiffAt_map_inverse` `RingHomCompTriple.right_ids` `RingHomInvPair.ids` `trivialization_linear` `instMemTrivializationAtlasTrivializationAt` `FiberBundle.mem_baseSet_trivializationAt'` `RingHomCompTriple.ids` `ContinuousLinearMap.inCoordinates_eq` `ContinuousLinearMap.IsInvertible.comp` `ContinuousLinearMap.isInvertible_equiv` `congr_of_eventuallyEq_of_mem` `nhdsWithin_le_nhds` `IsOpen.mem_nhds` `Trivialization.open_baseSet` `ContinuousWithinAt.preimage_mem_nhdsWithin` `ContMDiffWithinAt.continuousWithinAt` `Filter.mp_mem` `Filter.univ_mem'` `ContinuousLinearMap.inverse_equiv_comp` `ContinuousLinearMap.comp.congr_simp` `ContinuousLinearMap.inverse_comp_equiv` `clm_apply_of_inCoordinates` `mdifferentiableWithinAt_id`
`mpullbackWithin_vectorField_inter_of_eq` 📖	mathematical	`MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContMDiffWithinAt` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderivWithin` `Set` `Set.instMembership` `UniqueMDiffOn` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat`	`VectorField.mpullbackWithin` `Set.instInter` `Set.preimage`	—	`Nat.instAtLeastTwoHAddOfNat` `IsManifold.instOfNatWithTopENat_1` `mpullbackWithin_vectorField_inter`
`mpullback_vectorField_preimage` 📖	mathematical	`MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContMDiffAt` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderiv` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat`	`VectorField.mpullback` `Set.preimage`	—	`Nat.instAtLeastTwoHAddOfNat` `IsManifold.instOfNatWithTopENat_1` `VectorField.mpullbackWithin_univ` `Set.univ_inter` `mpullbackWithin_vectorField_inter` `Set.mem_univ` `uniqueMDiffOn_univ`
`mpullback_vectorField_preimage_of_eq` 📖	mathematical	`MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `ContMDiffAt` `ContinuousLinearMap.IsInvertible` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderiv` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat`	`VectorField.mpullback` `Set.preimage`	—	`Nat.instAtLeastTwoHAddOfNat` `IsManifold.instOfNatWithTopENat_1` `mpullback_vectorField_preimage`

VectorField

Definitions

Name	Category	Theorems
`mpullback` 📖	CompOp	31 math math: `mpullback_id`, `mpullback_mlieBracketWithin`, `mpullback_eq_pullback`, `MDifferentiableAt.mpullback_vectorField`, `mpullback_add_apply`, `mpullback_smul_apply`, `addInvariantVectorField_eq_mpullback`, `MDifferentiable.mpullback_vectorField`, `ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin_of_eq`, `ContMDiffWithinAt.mpullback_vectorField_preimage`, `mpullback_apply`, `mpullback_zero`, `mpullback_mlieBracket`, `mlieBracketWithin_def`, `ContMDiffWithinAt.mpullback_vectorField_preimage_of_eq`, `mpullbackWithin_univ`, `mpullback_addInvariantVectorField`, `eventuallyEq_mpullback_mpullbackWithin_extChartAt`, `MDifferentiableOn.mpullback_vectorField_preimage`, `mpullback_add`, `MDifferentiableWithinAt.mpullback_vectorField_preimage`, `mpullback_smul`, `mpullback_neg_apply`, `ContMDiffOn.mpullback_vectorField_preimage`, `MDifferentiableWithinAt.mpullback_vectorField_preimage_of_eq`, `mpullback_neg`, `ContMDiffAt.mpullback_vectorField_preimage`, `mpullback_mulInvariantVectorField`, `mulInvariantVectorField_eq_mpullback`, `ContMDiff.mpullback_vectorField`, `ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin`
`mpullbackWithin` 📖	CompOp	34 math math: `mpullbackWithin_comp_of_left`, `MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField`, `mpullbackWithin_add`, `mpullbackWithin_smul`, `mpullbackWithin_comp_of_right`, `mpullbackWithin_mlieBracketWithin'`, `ContMDiffWithinAt.mpullbackWithin_vectorField_inter`, `mpullbackWithin_neg_apply`, `ContMDiffOn.mpullbackWithin_vectorField_inter`, `MDifferentiableWithinAt.mpullbackWithin_vectorField_inter_of_eq`, `mpullbackWithin_neg`, `mlieBracketWithin_def`, `mpullbackWithin_univ`, `mpullbackWithin_zero`, `ContMDiffWithinAt.mpullbackWithin_vectorField'`, `mpullbackWithin_smul_apply`, `mpullbackWithin_id`, `eventuallyEq_mpullback_mpullbackWithin_extChartAt`, `ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem_of_eq`, `contMDiffWithinAt_mpullbackWithin_extChartAt_symm`, `mpullbackWithin_mlieBracketWithin`, `MDifferentiableOn.mpullbackWithin_vectorField_inter`, `ContMDiffWithinAt.mpullbackWithin_vectorField_inter_of_eq`, `mpullbackWithin_eq_pullbackWithin`, `mpullbackWithin_apply`, `MDifferentiableWithinAt.mpullbackWithin_vectorField_inter`, `mpullbackWithin_mlieBracketWithin_of_isSymmSndFDerivWithinAt`, `ContMDiffWithinAt.mpullbackWithin_vectorField`, `ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq`, `mlieBracketWithin_apply`, `ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem`, `eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm`, `ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq'`, `mpullbackWithin_add_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contMDiffWithinAt_mpullbackWithin_extChartAt_symm` 📖	mathematical	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `UniqueMDiffOn` `Set` `Set.instMembership` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`modelWithCornersSelf` `chartedSpaceSelf` `instIsManifoldOfNatWithTopENatOfMinSmoothness_1` `instIsManifoldMinSmoothnessOfNatWithTopENat_1` `instIsManifoldMinSmoothnessOfNatWithTopENat` `IsManifold.instOfTopWithTopENat` `minSmoothness` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat` `instIsManifoldModelSpace` `Top.top` `WithTop.top` `mpullbackWithin` `PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt` `Set.range` `ModelWithCorners.toFun'` `Set.instInter` `PartialEquiv.target` `Set.preimage`	—	`ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq'` `instIsManifoldOfNatWithTopENatOfMinSmoothness_1` `instIsManifoldMinSmoothnessOfNatWithTopENat_1` `instIsManifoldMinSmoothnessOfNatWithTopENat` `IsManifold.instOfTopWithTopENat` `Nat.instAtLeastTwoHAddOfNat` `instIsManifoldModelSpace` `contMDiffWithinAt_extChartAt_symm_range_self` `isInvertible_mfderivWithin_extChartAt_symm` `mem_extChartAt_target` `ModelWithCorners.target_eq` `ModelWithCorners.left_inv` `OpenPartialHomeomorph.left_inv` `UniqueMDiffOn.uniqueMDiffOn_target_inter` `Set.MapsTo.preimage_mem_nhdsWithin` `Set.MapsTo.mono_left` `Set.mapsTo_preimage` `Set.inter_subset_right` `Set.Subset.trans` `Set.inter_subset_left` `extChartAt_target_subset_range` `extChartAt_to_inv`
`eventuallyEq_mpullback_mpullbackWithin_extChartAt` 📖	mathematical	—	`Filter.EventuallyEq` `nhdsWithin` `mpullback` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `extChartAt` `mpullbackWithin` `PartialEquiv.symm` `Set.range` `ModelWithCorners.toFun'`	—	`nhdsWithin_le_nhds` `Filter.mp_mem` `extChartAt_source_mem_nhds` `Filter.univ_mem'` `PartialEquiv.left_inv` `mpullback_apply` `mpullbackWithin_apply` `RingHomCompTriple.ids` `ContinuousLinearMap.IsInvertible.inverse_comp_apply_of_right` `isInvertible_mfderiv_extChartAt` `mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt'` `ContinuousLinearMap.inverse_id`
`eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm` 📖	mathematical	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `UniqueMDiffOn` `Set` `Set.instMembership` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`Filter.Eventually` `modelWithCornersSelf` `chartedSpaceSelf` `instIsManifoldOfNatWithTopENatOfMinSmoothness_1` `instIsManifoldMinSmoothnessOfNatWithTopENat_1` `instIsManifoldMinSmoothnessOfNatWithTopENat` `IsManifold.instOfTopWithTopENat` `minSmoothness` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat` `instIsManifoldModelSpace` `Top.top` `WithTop.top` `mpullbackWithin` `PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt` `Set.range` `ModelWithCorners.toFun'` `Set.instInter` `PartialEquiv.target` `Set.preimage` `nhdsWithin`	—	`instIsManifoldOfNatWithTopENatOfMinSmoothness_1` `instIsManifoldMinSmoothnessOfNatWithTopENat_1` `instIsManifoldMinSmoothnessOfNatWithTopENat` `IsManifold.instOfTopWithTopENat` `Nat.instAtLeastTwoHAddOfNat` `instIsManifoldModelSpace` `nhdsWithin_mono` `Set.subset_insert` `contMDiffWithinAt_iff_contMDiffWithinAt_nhdsWithin` `Bundle.TotalSpace.isManifold` `TangentSpace.vectorBundle` `instContMDiffVectorBundleOfTopWithTopENat` `instContMDiffVectorBundleTopWithTopENatTangentSpaceOfIsManifold` `contMDiffWithinAt_mpullbackWithin_extChartAt_symm` `ContinuousWithinAt.preimage_mem_nhdsWithin''` `ContinuousAt.continuousWithinAt` `continuousAt_extChartAt` `nhdsWithin_le_iff` `Filter.mp_mem` `nhdsWithin_le_nhds` `extChartAt_source_mem_nhds` `self_mem_nhdsWithin` `Filter.univ_mem'` `ModelWithCorners.target_eq` `ModelWithCorners.left_inv` `ModelWithCorners.source_eq` `Set.inter_univ` `OpenPartialHomeomorph.left_inv`
`mpullbackWithin_add` 📖	mathematical	—	`mpullbackWithin` `Pi.instAdd` `TangentSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `instTopologicalSpaceTangentSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`map_add` `SemilinearMapClass.toAddHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`
`mpullbackWithin_add_apply` 📖	mathematical	—	`mpullbackWithin` `Pi.instAdd` `TangentSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `instTopologicalSpaceTangentSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`map_add` `SemilinearMapClass.toAddHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`
`mpullbackWithin_apply` 📖	mathematical	—	`mpullbackWithin` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.funLike` `ContinuousLinearMap.inverse` `mfderivWithin`	—	—
`mpullbackWithin_comp_of_left` 📖	mathematical	`MDifferentiableWithinAt` `Set.MapsTo` `UniqueMDiffWithinAt` `ContinuousLinearMap.IsInvertible` `TangentSpace` `instTopologicalSpaceTangentSpace` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderivWithin`	`mpullbackWithin`	—	`mdifferentiableWithinAt_of_isInvertible_mfderivWithin` `RingHomCompTriple.ids` `mfderivWithin_comp` `ContinuousLinearMap.IsInvertible.inverse_comp_apply_of_left`
`mpullbackWithin_comp_of_right` 📖	mathematical	`MDifferentiableWithinAt` `Set.MapsTo` `UniqueMDiffWithinAt` `ContinuousLinearMap.IsInvertible` `TangentSpace` `instTopologicalSpaceTangentSpace` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `mfderivWithin`	`mpullbackWithin`	—	`mdifferentiableWithinAt_of_isInvertible_mfderivWithin` `RingHomCompTriple.ids` `mfderivWithin_comp` `ContinuousLinearMap.IsInvertible.inverse_comp_apply_of_right`
`mpullbackWithin_eq_pullbackWithin` 📖	mathematical	—	`mpullbackWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `pullbackWithin`	—	`mfderivWithin_eq_fderivWithin`
`mpullbackWithin_id` 📖	mathematical	`UniqueMDiffWithinAt`	`mpullbackWithin`	—	`mfderivWithin_id` `ContinuousLinearMap.inverse_id`
`mpullbackWithin_neg` 📖	mathematical	—	`mpullbackWithin` `Pi.instNeg` `TangentSpace` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace`	—	`map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`
`mpullbackWithin_neg_apply` 📖	mathematical	—	`mpullbackWithin` `Pi.instNeg` `TangentSpace` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace`	—	`map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`
`mpullbackWithin_smul` 📖	mathematical	—	`mpullbackWithin` `Pi.instSMul` `TangentSpace` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `instModuleTangentSpace`	—	`map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`
`mpullbackWithin_smul_apply` 📖	mathematical	—	`mpullbackWithin` `Pi.instSMul` `TangentSpace` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `instModuleTangentSpace` `AddZero.toZero` `AddZeroClass.toAddZero` `ENormedAddMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toENormedAddMonoid`	—	`map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`
`mpullbackWithin_univ` 📖	mathematical	—	`mpullbackWithin` `Set.univ` `mpullback`	—	`mfderivWithin_univ`
`mpullbackWithin_zero` 📖	mathematical	—	`mpullbackWithin` `Pi.instZero` `TangentSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`
`mpullback_add` 📖	mathematical	—	`mpullback` `Pi.instAdd` `TangentSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `instTopologicalSpaceTangentSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`map_add` `SemilinearMapClass.toAddHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`
`mpullback_add_apply` 📖	mathematical	—	`mpullback` `Pi.instAdd` `TangentSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `instTopologicalSpaceTangentSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`map_add` `SemilinearMapClass.toAddHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`
`mpullback_apply` 📖	mathematical	—	`mpullback` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.funLike` `ContinuousLinearMap.inverse` `mfderiv`	—	—
`mpullback_eq_pullback` 📖	mathematical	—	`mpullback` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `pullback`	—	`mpullbackWithin_eq_pullbackWithin`
`mpullback_id` 📖	mathematical	—	`mpullback`	—	`mfderiv_id` `ContinuousLinearMap.inverse_id`
`mpullback_neg` 📖	mathematical	—	`mpullback` `Pi.instNeg` `TangentSpace` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace`	—	`map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`
`mpullback_neg_apply` 📖	mathematical	—	`mpullback` `Pi.instNeg` `TangentSpace` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace`	—	`map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`
`mpullback_smul` 📖	mathematical	—	`mpullback` `Pi.instSMul` `TangentSpace` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `instModuleTangentSpace`	—	`map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`
`mpullback_smul_apply` 📖	mathematical	—	`mpullback` `Pi.instSMul` `TangentSpace` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `instModuleTangentSpace` `AddZero.toZero` `AddZeroClass.toAddZero` `ENormedAddMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toENormedAddMonoid`	—	`map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`
`mpullback_zero` 📖	mathematical	—	`mpullback` `Pi.instZero` `TangentSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace`	—	`mpullbackWithin_zero`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsManifoldMinSmoothnessOfNatWithTopENat` 📖	mathematical	—	`IsManifold` `minSmoothness` `WithTop` `ENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `IsManifold.of_le` `minSmoothness_monotone` `WithTop.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `WithTop.zeroLEOneClass` `IsOrderedRing.toZeroLEOneClass` `WithTop.charZero`
`instIsManifoldMinSmoothnessOfNatWithTopENat_1` 📖	mathematical	—	`IsManifold` `minSmoothness` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`Nat.instAtLeastTwoHAddOfNat` `IsManifold.of_le` `minSmoothness_monotone` `Nat.cast_one` `WithTop.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `WithTop.zeroLEOneClass` `IsOrderedRing.toZeroLEOneClass` `WithTop.charZero`
`instIsManifoldOfNatWithTopENatOfMinSmoothness` 📖	mathematical	—	`IsManifold`	—	`IsManifold.of_le` `le_minSmoothness`
`instIsManifoldOfNatWithTopENatOfMinSmoothness_1` 📖	mathematical	—	`IsManifold` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`IsManifold.of_le` `le_minSmoothness`

---

← Back to Index