BumpFunction

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

Statistics

Metric	Count
Definitions `SmoothBumpFunction`, `instCoeFunForallReal`, `toContDiffBump`, `toFun`, `updateRIn`	5
Theorems `ball_inter_range_eq_ball_inter_target`, `ball_subset`, `c_mem_support`, `closedBall_subset`, `coe_def`, `contMDiff`, `contMDiffAt`, `contMDiff_smul`, `continuous`, `eqOn_source`, `eq_one`, `eventuallyEq_of_mem_source`, `eventuallyEq_one`, `eventuallyEq_one_of_dist_lt`, `exists_r_pos_lt_subset_ball`, `hasCompactSupport`, `image_eq_inter_preimage_of_subset_support`, `instNonempty`, `isClosed_image_of_isClosed`, `isClosed_symm_image_closedBall`, `isCompact_symm_image_closedBall`, `isOpen_support`, `le_one`, `mem_Icc`, `nhdsWithin_range_basis`, `nhds_basis_support`, `nhds_basis_tsupport`, `nonempty_support`, `nonneg`, `one_of_dist_le`, `rOut_pos`, `support_eq_inter_preimage`, `support_eq_symm_image`, `support_mem_nhds`, `support_subset_source`, `support_updateRIn`, `tsupport_mem_nhds`, `tsupport_subset_chartAt_source`, `tsupport_subset_extChartAt_source`, `tsupport_subset_symm_image_closedBall`, `updateRIn_rIn`, `updateRIn_rOut`	42
Total	47

SmoothBumpFunction

Definitions

Name	Category	Theorems
`instCoeFunForallReal` 📖	CompOp	—
`toContDiffBump` 📖	CompOp	15 math math: `support_eq_symm_image`, `rOut_pos`, `exists_r_pos_lt_subset_ball`, `support_eq_inter_preimage`, `tsupport_subset_symm_image_closedBall`, `ball_subset`, `eqOn_source`, `isClosed_symm_image_closedBall`, `eventuallyEq_of_mem_source`, `coe_def`, `nhdsWithin_range_basis`, `image_eq_inter_preimage_of_subset_support`, `closedBall_subset`, `isCompact_symm_image_closedBall`, `ball_inter_range_eq_ball_inter_target`
`toFun` 📖	CompOp	43 math math: `SmoothBumpCovering.toSmoothPartitionOfUnity_eq_mul_prod`, `support_eq_symm_image`, `SmoothBumpCovering.mem_support_ind`, `SmoothBumpCovering.IsSubordinate.support_subset`, `le_one`, `continuous`, `SmoothBumpCovering.toSmoothPartitionOfUnity_apply`, `support_mem_nhds`, `support_eq_inter_preimage`, `tsupport_subset_symm_image_closedBall`, `SmoothBumpCovering.locallyFinite'`, `contMDiffAt`, `hasCompactSupport`, `SmoothBumpCovering.sum_toSmoothPartitionOfUnity_eq`, `tsupport_subset_chartAt_source`, `eqOn_source`, `mem_Icc`, `tsupport_mem_nhds`, `nhds_basis_support`, `SmoothBumpCovering.point_finite`, `SmoothBumpCovering.eventuallyEq_one`, `c_mem_support`, `SmoothBumpCovering.exists_finset_toSmoothPartitionOfUnity_eventuallyEq`, `eventuallyEq_of_mem_source`, `contMDiff_smul`, `coe_def`, `SmoothBumpCovering.locallyFinite`, `isOpen_support`, `SmoothBumpCovering.eventuallyEq_one'`, `one_of_dist_le`, `SmoothBumpCovering.apply_ind`, `SmoothBumpCovering.support_toSmoothPartitionOfUnity_subset`, `eventuallyEq_one_of_dist_lt`, `contMDiff`, `tsupport_subset_extChartAt_source`, `support_subset_source`, `nonneg`, `eventuallyEq_one`, `support_updateRIn`, `SmoothBumpCovering.embeddingPiTangent_coe`, `eq_one`, `nhds_basis_tsupport`, `nonempty_support`
`updateRIn` 📖	CompOp	3 math math: `updateRIn_rOut`, `updateRIn_rIn`, `support_updateRIn`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ball_inter_range_eq_ball_inter_target` 📖	mathematical	—	`Set` `Set.instInter` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extChartAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `ContDiffBump.rOut` `toContDiffBump` `Set.range` `ModelWithCorners.toFun'` `PartialEquiv.target`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `Set.subset_inter` `Set.inter_subset_left` `ball_subset` `Set.inter_subset_inter_right` `extChartAt_target_subset_range`
`ball_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.instInter` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extChartAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `ContDiffBump.rOut` `toContDiffBump` `Set.range` `ModelWithCorners.toFun'` `PartialEquiv.target`	—	`Set.Subset.trans` `Set.inter_subset_inter_left` `Metric.ball_subset_closedBall` `closedBall_subset`
`c_mem_support` 📖	mathematical	—	`Set` `Set.instMembership` `Function.support` `Real` `Real.instZero` `toFun`	—	`mem_of_mem_nhds` `support_mem_nhds`
`closedBall_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.instInter` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extChartAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `ContDiffBump.rOut` `toContDiffBump` `Set.range` `ModelWithCorners.toFun'` `PartialEquiv.target`	—	—
`coe_def` 📖	mathematical	—	`toFun` `Set.indicator` `Real` `Real.instZero` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt` `ContDiffBump.toFun` `ExistsContDiffBumpBase.instHasContDiffBumpOfFiniteDimensionalReal` `PartialEquiv.toFun` `extChartAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `toContDiffBump`	—	—
`contMDiff` 📖	mathematical	—	`ContMDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `modelWithCornersSelf` `Real.pseudoMetricSpace` `chartedSpaceSelf` `WithTop.some` `ENat` `Top.top` `instTopENat` `toFun`	—	`contMDiff_of_tsupport` `tsupport_subset_chartAt_source` `ContMDiffAt.congr_of_eventuallyEq` `ExistsContDiffBumpBase.instHasContDiffBumpOfFiniteDimensionalReal` `ContMDiffAt.comp` `ContDiffAt.contMDiffAt` `ContDiffBump.contDiffAt` `contMDiffAt_extChartAt'` `Set.EqOn.eventuallyEq_of_mem` `eqOn_source` `IsOpen.mem_nhds` `OpenPartialHomeomorph.open_source`
`contMDiffAt` 📖	mathematical	—	`ContMDiffAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `modelWithCornersSelf` `Real.pseudoMetricSpace` `chartedSpaceSelf` `WithTop.some` `ENat` `Top.top` `instTopENat` `toFun`	—	`ContMDiff.contMDiffAt` `contMDiff`
`contMDiff_smul` 📖	mathematical	`ContMDiffOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `WithTop.some` `ENat` `Top.top` `instTopENat` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt`	`ContMDiff` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `toFun`	—	`contMDiff_of_tsupport` `tsupport_subset_chartAt_source` `tsupport_smul_subset_left` `ContMDiffAt.smul` `contMDiffAt` `ContMDiffWithinAt.contMDiffAt` `IsOpen.mem_nhds` `OpenPartialHomeomorph.open_source`
`continuous` 📖	mathematical	—	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `toFun`	—	`ContMDiff.continuous` `contMDiff`
`eqOn_source` 📖	mathematical	—	`Set.EqOn` `Real` `toFun` `ContDiffBump.toFun` `ExistsContDiffBumpBase.instHasContDiffBumpOfFiniteDimensionalReal` `PartialEquiv.toFun` `extChartAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `toContDiffBump` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt`	—	`Set.eqOn_indicator` `ExistsContDiffBumpBase.instHasContDiffBumpOfFiniteDimensionalReal`
`eq_one` 📖	mathematical	—	`toFun` `Real` `Real.instOne`	—	`Filter.EventuallyEq.eq_of_nhds` `eventuallyEq_one`
`eventuallyEq_of_mem_source` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt`	`Filter.EventuallyEq` `Real` `nhds` `toFun` `ContDiffBump.toFun` `ExistsContDiffBumpBase.instHasContDiffBumpOfFiniteDimensionalReal` `PartialEquiv.toFun` `extChartAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `toContDiffBump`	—	`Set.EqOn.eventuallyEq_of_mem` `ExistsContDiffBumpBase.instHasContDiffBumpOfFiniteDimensionalReal` `eqOn_source` `IsOpen.mem_nhds` `OpenPartialHomeomorph.open_source`
`eventuallyEq_one` 📖	mathematical	—	`Filter.EventuallyEq` `Real` `nhds` `toFun` `Pi.instOne` `Real.instOne`	—	`eventuallyEq_one_of_dist_lt` `mem_chart_source` `dist_self` `ContDiffBump.rIn_pos`
`eventuallyEq_one_of_dist_lt` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt` `Real` `Real.instLT` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extChartAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `ContDiffBump.rIn` `toContDiffBump`	`Filter.EventuallyEq` `nhds` `toFun` `Pi.instOne` `Real.instOne`	—	`Filter.mp_mem` `IsOpen.mem_nhds` `isOpen_extChartAt_preimage` `Metric.isOpen_ball` `Filter.univ_mem'` `one_of_dist_le` `le_of_lt`
`exists_r_pos_lt_subset_ball` 📖	mathematical	`Set` `Set.instHasSubset` `Function.support` `Real` `Real.instZero` `toFun`	`Set.instMembership` `Set.Ioo` `Real.instPreorder` `ContDiffBump.rOut` `PartialEquiv.toFun` `extChartAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `toContDiffBump` `Set.instInter` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt` `Set.preimage` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`isClosed_image_of_isClosed` `exists_pos_lt_subset_ball` `FiniteDimensional.proper_real` `rOut_pos` `Set.image_subset_iff` `Set.subset_inter_iff` `support_eq_inter_preimage` `Set.subset_inter`
`hasCompactSupport` 📖	mathematical	—	`HasCompactSupport` `Real` `Real.instZero` `toFun`	—	`IsCompact.of_isClosed_subset` `isCompact_symm_image_closedBall` `isClosed_closure` `tsupport_subset_symm_image_closedBall`
`image_eq_inter_preimage_of_subset_support` 📖	mathematical	`Set` `Set.instHasSubset` `Function.support` `Real` `Real.instZero` `toFun`	`Set.image` `PartialEquiv.toFun` `extChartAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Set.instInter` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContDiffBump.rOut` `toContDiffBump` `Set.range` `ModelWithCorners.toFun'` `Set.preimage` `PartialEquiv.symm`	—	`Set.image_subset_iff` `extChartAt_source` `Set.subset_inter_iff` `support_eq_inter_preimage` `Set.Subset.antisymm` `Set.subset_inter` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Metric.ball_subset_closedBall` `Set.mem_range_self` `PartialEquiv.image_eq_target_inter_inv_preimage` `Set.inter_subset_right` `Set.Subset.trans` `Set.inter_subset_inter_left` `closedBall_subset` `subset_refl` `Set.instReflSubset`
`instNonempty` 📖	mathematical	—	`SmoothBumpFunction`	—	`Filter.HasBasis.nonempty` `nhdsWithin_range_basis`
`isClosed_image_of_isClosed` 📖	mathematical	`Set` `Set.instHasSubset` `Function.support` `Real` `Real.instZero` `toFun`	`IsClosed` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.image` `PartialEquiv.toFun` `extChartAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField`	—	`image_eq_inter_preimage_of_subset_support` `ContinuousOn.preimage_isClosed_of_isClosed` `ContinuousOn.mono` `continuousOn_extChartAt_symm` `closedBall_subset` `IsClosed.inter` `Metric.isClosed_closedBall` `ModelWithCorners.isClosed_range`
`isClosed_symm_image_closedBall` 📖	mathematical	—	`IsClosed` `Set.image` `PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Set` `Set.instInter` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContDiffBump.rOut` `toContDiffBump` `Set.range` `ModelWithCorners.toFun'`	—	`IsCompact.isClosed` `isCompact_symm_image_closedBall`
`isCompact_symm_image_closedBall` 📖	mathematical	—	`IsCompact` `Set.image` `PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Set` `Set.instInter` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContDiffBump.rOut` `toContDiffBump` `Set.range` `ModelWithCorners.toFun'`	—	`IsCompact.image_of_continuousOn` `IsCompact.inter_right` `ProperSpace.isCompact_closedBall` `FiniteDimensional.proper_real` `ModelWithCorners.isClosed_range` `ContinuousOn.mono` `continuousOn_extChartAt_symm` `closedBall_subset`
`isOpen_support` 📖	mathematical	—	`IsOpen` `Function.support` `Real` `Real.instZero` `toFun`	—	`support_eq_inter_preimage` `isOpen_extChartAt_preimage` `Metric.isOpen_ball`
`le_one` 📖	mathematical	—	`Real` `Real.instLE` `toFun` `Real.instOne`	—	`mem_Icc`
`mem_Icc` 📖	mathematical	—	`Real` `Set` `Set.instMembership` `Set.Icc` `Real.instPreorder` `Real.instZero` `Real.instOne` `toFun`	—	`ExistsContDiffBumpBase.instHasContDiffBumpOfFiniteDimensionalReal` `Set.indicator_eq_zero_or_self` `Set.left_mem_Icc` `zero_le_one` `Real.instZeroLEOneClass` `ContDiffBump.nonneg` `ContDiffBump.le_one`
`nhdsWithin_range_basis` 📖	mathematical	—	`Filter.HasBasis` `SmoothBumpFunction` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extChartAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Set.range` `ModelWithCorners.toFun'` `Set` `Set.instInter` `Metric.closedBall` `ContDiffBump.rOut` `toContDiffBump`	—	`Filter.HasBasis.to_hasBasis'` `Filter.HasBasis.restrict_subset` `nhdsWithin_hasBasis` `Metric.nhds_basis_closedBall` `extChartAt_target_mem_nhdsWithin` `Nat.instAtLeastTwoHAddOfNat` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `half_lt_self` `Set.Subset.rfl` `Filter.inter_mem` `mem_nhdsWithin_of_mem_nhds` `Metric.closedBall_mem_nhds` `rOut_pos` `self_mem_nhdsWithin`
`nhds_basis_support` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`Filter.HasBasis` `SmoothBumpFunction` `Set.instHasSubset` `tsupport` `Real` `Real.instZero` `toFun` `Function.support`	—	`Filter.HasBasis.to_hasBasis'` `Filter.HasBasis.restrict_subset` `nhds_basis_tsupport` `subset_closure` `support_mem_nhds`
`nhds_basis_tsupport` 📖	mathematical	—	`Filter.HasBasis` `SmoothBumpFunction` `nhds` `tsupport` `Real` `Real.instZero` `toFun`	—	`map_extChartAt_symm_nhdsWithin_range` `Filter.HasBasis.map` `nhdsWithin_range_basis` `Filter.HasBasis.to_hasBasis'` `tsupport_subset_symm_image_closedBall` `tsupport_mem_nhds`
`nonempty_support` 📖	mathematical	—	`Set.Nonempty` `Function.support` `Real` `Real.instZero` `toFun`	—	`c_mem_support`
`nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `toFun`	—	`mem_Icc`
`one_of_dist_le` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt` `Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialEquiv.toFun` `extChartAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `ContDiffBump.rIn` `toContDiffBump`	`toFun` `Real.instOne`	—	`ExistsContDiffBumpBase.instHasContDiffBumpOfFiniteDimensionalReal` `eqOn_source` `ContDiffBump.one_of_mem_closedBall`
`rOut_pos` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `ContDiffBump.rOut` `PartialEquiv.toFun` `extChartAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `toContDiffBump`	—	`ContDiffBump.rOut_pos`
`support_eq_inter_preimage` 📖	mathematical	—	`Function.support` `Real` `Real.instZero` `toFun` `Set` `Set.instInter` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt` `Set.preimage` `PartialEquiv.toFun` `extChartAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContDiffBump.rOut` `toContDiffBump`	—	`ExistsContDiffBumpBase.instHasContDiffBumpOfFiniteDimensionalReal` `coe_def` `Set.support_indicator` `Function.support_comp_eq_preimage` `extChartAt_source` `PartialEquiv.symm_image_target_inter_eq'` `ContDiffBump.support_eq`
`support_eq_symm_image` 📖	mathematical	—	`Function.support` `Real` `Real.instZero` `toFun` `Set.image` `PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Set` `Set.instInter` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContDiffBump.rOut` `toContDiffBump` `Set.range` `ModelWithCorners.toFun'`	—	`support_eq_inter_preimage` `extChartAt_source` `PartialEquiv.symm_image_target_inter_eq'` `Set.inter_comm` `ball_inter_range_eq_ball_inter_target`
`support_mem_nhds` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `Function.support` `Real` `Real.instZero` `toFun`	—	`Filter.Eventually.mono` `eventuallyEq_one` `one_ne_zero` `NeZero.charZero_one` `RCLike.charZero_rclike`
`support_subset_source` 📖	mathematical	—	`Set` `Set.instHasSubset` `Function.support` `Real` `Real.instZero` `toFun` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt`	—	`support_eq_inter_preimage` `extChartAt_source` `Set.inter_subset_left`
`support_updateRIn` 📖	mathematical	`Real` `Set` `Set.instMembership` `Set.Ioo` `Real.instPreorder` `Real.instZero` `ContDiffBump.rOut` `PartialEquiv.toFun` `extChartAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `toContDiffBump`	`Function.support` `toFun` `updateRIn`	—	`support_eq_inter_preimage`
`tsupport_mem_nhds` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `tsupport` `Real` `Real.instZero` `toFun`	—	`Filter.mem_of_superset` `support_mem_nhds` `subset_closure`
`tsupport_subset_chartAt_source` 📖	mathematical	—	`Set` `Set.instHasSubset` `tsupport` `Real` `Real.instZero` `toFun` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt`	—	`extChartAt_source` `tsupport_subset_extChartAt_source`
`tsupport_subset_extChartAt_source` 📖	mathematical	—	`Set` `Set.instHasSubset` `tsupport` `Real` `Real.instZero` `toFun` `PartialEquiv.source` `extChartAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField`	—	`tsupport_subset_symm_image_closedBall` `Set.image_mono` `closedBall_subset` `PartialEquiv.symm_image_target_eq_source`
`tsupport_subset_symm_image_closedBall` 📖	mathematical	—	`Set` `Set.instHasSubset` `tsupport` `Real` `Real.instZero` `toFun` `Set.image` `PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Set.instInter` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContDiffBump.rOut` `toContDiffBump` `Set.range` `ModelWithCorners.toFun'`	—	`tsupport.eq_1` `support_eq_symm_image` `closure_minimal` `Set.image_mono` `Set.inter_subset_inter_left` `Metric.ball_subset_closedBall` `isClosed_symm_image_closedBall`
`updateRIn_rIn` 📖	mathematical	`Real` `Set` `Set.instMembership` `Set.Ioo` `Real.instPreorder` `Real.instZero` `ContDiffBump.rOut` `PartialEquiv.toFun` `extChartAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `toContDiffBump`	`ContDiffBump.rIn` `updateRIn`	—	—
`updateRIn_rOut` 📖	mathematical	`Real` `Set` `Set.instMembership` `Set.Ioo` `Real.instPreorder` `Real.instZero` `ContDiffBump.rOut` `PartialEquiv.toFun` `extChartAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `toContDiffBump`	`updateRIn`	—	—

(root)

Definitions

Name	Category	Theorems
`SmoothBumpFunction` 📖	CompData	4 math math: `SmoothBumpFunction.nhds_basis_support`, `SmoothBumpFunction.instNonempty`, `SmoothBumpFunction.nhdsWithin_range_basis`, `SmoothBumpFunction.nhds_basis_tsupport`

---

← Back to Index