ZeroAtInfty

📁 Source: Mathlib/Topology/ContinuousMap/ZeroAtInfty.lean

Statistics

Metric	Count
Definitions `«termC₀(_,_)»`»), `«term_→C₀_»`, `ZeroAtInftyContinuousMap`, `liftZeroAtInfty`, `comp`, `compAddMonoidHom`, `compLinearMap`, `compMulHom`, `compNonUnitalAlgHom`, `copy`, `instAdd`, `instAddCommGroup`, `instAddCommMonoid`, `instAddGroup`, `instAddMonoid`, `instAddZeroClass`, `instCoeTC`, `instFunLike`, `instInhabited`, `instMetricSpace`, `instModule`, `instMul`, `instMulActionWithZero`, `instMulZeroClass`, `instNeg`, `instNonUnitalCommRing`, `instNonUnitalCommSemiring`, `instNonUnitalNonAssocRing`, `instNonUnitalNonAssocSemiring`, `instNonUnitalNormedCommRing`, `instNonUnitalNormedRing`, `instNonUnitalRing`, `instNonUnitalSeminormedCommRing`, `instNonUnitalSeminormedRing`, `instNonUnitalSemiring`, `instNormedAddCommGroup`, `instNormedSpace`, `instPseudoMetricSpace`, `instSMul`, `instSMulWithZero`, `instSemigroupWithZero`, `instSeminormedAddCommGroup`, `instStar`, `instStarAddMonoid`, `instStarRing`, `instSub`, `instZero`, `toBCF`, `toContinuousMap`, `ZeroAtInftyContinuousMapClass`	50
Theorems `liftZeroAtInfty_apply_toFun`, `liftZeroAtInfty_symm_apply`, `add_apply`, `bounded`, `coe_add`, `coe_comp_to_continuous_fun`, `coe_copy`, `coe_mk`, `coe_mul`, `coe_neg`, `coe_smul`, `coe_star`, `coe_sub`, `coe_toContinuousMap`, `coe_zero`, `comp_assoc`, `comp_id`, `copy_eq`, `dist_toBCF_eq_dist`, `eq_of_empty`, `ext`, `ext_iff`, `instBoundedContinuousMapClass`, `instCStarRing`, `instCompleteSpace`, `instIsCentralScalar`, `instIsScalarTower`, `instNormedStarGroup`, `instSMulCommClass`, `instStarModule`, `instZeroAtInftyContinuousMapClass`, `isBounded_image`, `isBounded_range`, `isClosed_range_toBCF`, `isometry_toBCF`, `mul_apply`, `neg_apply`, `norm_toBCF_eq_norm`, `smul_apply`, `star_apply`, `sub_apply`, `tendsto_iff_tendstoUniformly`, `toBCF_apply`, `toBCF_injective`, `uniformContinuous`, `ofCompact`, `zero_apply`, `zero_at_infty'`, `zero_comp`, `toContinuousMapClass`, `zero_at_infty`	51
Total	101

ZeroAtInfty

Definitions

Name	Category	Theorems
`«termC₀(_,_)»` 📖» "API Documentation")	CompOp	—
`«term_→C₀_»` 📖	CompOp	—

ZeroAtInftyContinuousMap

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	4 math math: `coe_comp_to_continuous_fun`, `comp_assoc`, `zero_comp`, `comp_id`
`compAddMonoidHom` 📖	CompOp	—
`compLinearMap` 📖	CompOp	—
`compMulHom` 📖	CompOp	—
`compNonUnitalAlgHom` 📖	CompOp	—
`copy` 📖	CompOp	2 math math: `copy_eq`, `coe_copy`
`instAdd` 📖	CompOp	2 math math: `add_apply`, `coe_add`
`instAddCommGroup` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	1 math math: `SchwartzMap.toZeroAtInftyCLM_apply`
`instAddGroup` 📖	CompOp	—
`instAddMonoid` 📖	CompOp	—
`instAddZeroClass` 📖	CompOp	2 math math: `instIsScalarTower`, `instSMulCommClass`
`instCoeTC` 📖	CompOp	—
`instFunLike` 📖	CompOp	29 math math: `add_apply`, `coe_smul`, `smul_apply`, `coe_mk`, `coe_comp_to_continuous_fun`, `coe_zero`, `ContinuousMap.liftZeroAtInfty_apply_toFun`, `zero_apply`, `toBCF_apply`, `neg_apply`, `sub_apply`, `instZeroAtInftyContinuousMapClass`, `isBounded_image`, `coe_mul`, `ContinuousMap.liftZeroAtInfty_symm_apply`, `ext_iff`, `coe_toContinuousMap`, `PadicInt.mahlerEquiv_apply`, `star_apply`, `isBounded_range`, `tendsto_iff_tendstoUniformly`, `PadicInt.mahlerEquiv_symm_apply`, `coe_sub`, `coe_add`, `SchwartzMap.toZeroAtInfty_apply`, `coe_neg`, `mul_apply`, `SchwartzMap.toZeroAtInftyCLM_apply`, `coe_star`
`instInhabited` 📖	CompOp	—
`instMetricSpace` 📖	CompOp	—
`instModule` 📖	CompOp	3 math math: `PadicInt.mahlerEquiv_apply`, `PadicInt.mahlerEquiv_symm_apply`, `SchwartzMap.toZeroAtInftyCLM_apply`
`instMul` 📖	CompOp	2 math math: `coe_mul`, `mul_apply`
`instMulActionWithZero` 📖	CompOp	—
`instMulZeroClass` 📖	CompOp	—
`instNeg` 📖	CompOp	2 math math: `neg_apply`, `coe_neg`
`instNonUnitalCommRing` 📖	CompOp	—
`instNonUnitalCommSemiring` 📖	CompOp	—
`instNonUnitalNonAssocRing` 📖	CompOp	—
`instNonUnitalNonAssocSemiring` 📖	CompOp	2 math math: `instIsScalarTower`, `instSMulCommClass`
`instNonUnitalNormedCommRing` 📖	CompOp	—
`instNonUnitalNormedRing` 📖	CompOp	1 math math: `instCStarRing`
`instNonUnitalRing` 📖	CompOp	—
`instNonUnitalSeminormedCommRing` 📖	CompOp	—
`instNonUnitalSeminormedRing` 📖	CompOp	—
`instNonUnitalSemiring` 📖	CompOp	—
`instNormedAddCommGroup` 📖	CompOp	—
`instNormedSpace` 📖	CompOp	—
`instPseudoMetricSpace` 📖	CompOp	5 math math: `dist_toBCF_eq_dist`, `instCompleteSpace`, `isometry_toBCF`, `tendsto_iff_tendstoUniformly`, `SchwartzMap.toZeroAtInftyCLM_apply`
`instSMul` 📖	CompOp	6 math math: `instIsCentralScalar`, `coe_smul`, `instIsScalarTower`, `smul_apply`, `instSMulCommClass`, `instStarModule`
`instSMulWithZero` 📖	CompOp	—
`instSemigroupWithZero` 📖	CompOp	—
`instSeminormedAddCommGroup` 📖	CompOp	4 math math: `instNormedStarGroup`, `norm_toBCF_eq_norm`, `PadicInt.mahlerEquiv_apply`, `PadicInt.mahlerEquiv_symm_apply`
`instStar` 📖	CompOp	3 math math: `instStarModule`, `star_apply`, `coe_star`
`instStarAddMonoid` 📖	CompOp	1 math math: `instNormedStarGroup`
`instStarRing` 📖	CompOp	1 math math: `instCStarRing`
`instSub` 📖	CompOp	2 math math: `sub_apply`, `coe_sub`
`instZero` 📖	CompOp	3 math math: `coe_zero`, `zero_apply`, `zero_comp`
`toBCF` 📖	CompOp	7 math math: `toBCF_injective`, `isClosed_range_toBCF`, `dist_toBCF_eq_dist`, `toBCF_apply`, `norm_toBCF_eq_norm`, `isometry_toBCF`, `SchwartzMap.toZeroAtInfty_toBCF`
`toContinuousMap` 📖	CompOp	2 math math: `zero_at_infty'`, `coe_toContinuousMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DFunLike.coe` `ZeroAtInftyContinuousMap` `AddZero.toZero` `AddZeroClass.toAddZero` `instFunLike` `instAdd` `AddZero.toAdd`	—	—
`bounded` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `DFunLike.coe`	—	`Filter.mem_cocompact` `Filter.tendsto_def` `ZeroAtInftyContinuousMapClass.zero_at_infty` `Metric.closedBall_mem_nhds` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Bornology.IsBounded.subset_closedBall` `IsCompact.isBounded` `IsCompact.image` `ContinuousMapClass.map_continuous` `ZeroAtInftyContinuousMapClass.toContinuousMapClass` `LE.le.trans` `Metric.mem_closedBall` `le_max_left` `Set.mem_preimage` `le_max_right` `dist_triangle` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Metric.mem_closedBall'`
`coe_add` 📖	mathematical	—	`DFunLike.coe` `ZeroAtInftyContinuousMap` `AddZero.toZero` `AddZeroClass.toAddZero` `instFunLike` `instAdd` `Pi.instAdd` `AddZero.toAdd`	—	—
`coe_comp_to_continuous_fun` 📖	mathematical	—	`DFunLike.coe` `ZeroAtInftyContinuousMap` `instFunLike` `comp` `CocompactMap` `CocompactMap.instFunLike`	—	—
`coe_copy` 📖	mathematical	`DFunLike.coe` `ZeroAtInftyContinuousMap` `instFunLike`	`copy`	—	—
`coe_mk` 📖	mathematical	`Continuous` `Filter.Tendsto` `Filter.cocompact` `nhds`	`DFunLike.coe` `ZeroAtInftyContinuousMap` `instFunLike`	—	—
`coe_mul` 📖	mathematical	—	`DFunLike.coe` `ZeroAtInftyContinuousMap` `MulZeroClass.toZero` `instFunLike` `instMul` `Pi.instMul` `MulZeroClass.toMul`	—	—
`coe_neg` 📖	mathematical	—	`DFunLike.coe` `ZeroAtInftyContinuousMap` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `instFunLike` `instNeg` `Pi.instNeg` `NegZeroClass.toNeg`	—	—
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `ZeroAtInftyContinuousMap` `instFunLike` `instSMul` `Function.hasSMul` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass`	—	—
`coe_star` 📖	mathematical	—	`DFunLike.coe` `ZeroAtInftyContinuousMap` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instFunLike` `Star.star` `instStar` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar`	—	—
`coe_sub` 📖	mathematical	—	`DFunLike.coe` `ZeroAtInftyContinuousMap` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `instFunLike` `instSub` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	—
`coe_toContinuousMap` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `toContinuousMap` `ZeroAtInftyContinuousMap` `instFunLike`	—	—
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `ZeroAtInftyContinuousMap` `instFunLike` `instZero` `Pi.instZero`	—	—
`comp_assoc` 📖	mathematical	—	`comp` `CocompactMap.comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `CocompactMap.id`	—	`ext`
`copy_eq` 📖	mathematical	`DFunLike.coe` `ZeroAtInftyContinuousMap` `instFunLike`	`copy`	—	`DFunLike.ext'`
`dist_toBCF_eq_dist` 📖	mathematical	—	`Dist.dist` `BoundedContinuousFunction` `BoundedContinuousFunction.instDist` `toBCF` `ZeroAtInftyContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `PseudoMetricSpace.toDist` `instPseudoMetricSpace`	—	—
`eq_of_empty` 📖	—	—	—	—	`ext`
`ext` 📖	—	`DFunLike.coe` `ZeroAtInftyContinuousMap` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `ZeroAtInftyContinuousMap` `instFunLike`	—	`ext`
`instBoundedContinuousMapClass` 📖	mathematical	—	`BoundedContinuousMapClass`	—	`ZeroAtInftyContinuousMapClass.toContinuousMapClass` `bounded`
`instCStarRing` 📖	mathematical	—	`CStarRing` `ZeroAtInftyContinuousMap` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `instNonUnitalNormedRing` `instStarRing` `NonUnitalRing.toNonUnitalSemiring` `NormedStarGroup.to_continuousStar` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `StarRing.toStarAddMonoid` `CStarRing.to_normedStarGroup` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing`	—	`NormedStarGroup.to_continuousStar` `CStarRing.to_normedStarGroup` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `CStarRing.norm_mul_self_le` `BoundedContinuousFunction.instCStarRing`
`instCompleteSpace` 📖	mathematical	—	`CompleteSpace` `ZeroAtInftyContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpace`	—	`completeSpace_iff_isComplete_range` `Isometry.isUniformInducing` `isometry_toBCF` `IsClosed.isComplete` `BoundedContinuousFunction.instCompleteSpace` `isClosed_range_toBCF`
`instIsCentralScalar` 📖	mathematical	—	`IsCentralScalar` `ZeroAtInftyContinuousMap` `instSMul` `MulOpposite` `MulOpposite.instZero` `ContinuousConstSMul.op` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass`	—	`ContinuousConstSMul.op` `ext` `IsCentralScalar.op_smul_eq_smul`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `ZeroAtInftyContinuousMap` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulActionWithZero.toSMulWithZero` `Semiring.toMonoidWithZero` `Module.toMulActionWithZero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `IsTopologicalSemiring.toContinuousAdd` `DistribSMul.toSMulZeroClass` `NonUnitalNonAssocSemiring.toDistribSMul` `instNonUnitalNonAssocSemiring`	—	`IsTopologicalSemiring.toContinuousAdd` `ext` `smul_eq_mul` `smul_assoc`
`instNormedStarGroup` 📖	mathematical	—	`NormedStarGroup` `ZeroAtInftyContinuousMap` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instSeminormedAddCommGroup` `instStarAddMonoid` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `NormedStarGroup.to_continuousStar` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`NormedStarGroup.to_continuousStar` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Eq.le` `norm_star` `BoundedContinuousFunction.instNormedStarGroup`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `ZeroAtInftyContinuousMap` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulActionWithZero.toSMulWithZero` `Semiring.toMonoidWithZero` `Module.toMulActionWithZero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `IsTopologicalSemiring.toContinuousAdd` `DistribSMul.toSMulZeroClass` `NonUnitalNonAssocSemiring.toDistribSMul` `instNonUnitalNonAssocSemiring`	—	`IsTopologicalSemiring.toContinuousAdd` `ext` `smul_eq_mul` `SMulCommClass.smul_comm`
`instStarModule` 📖	mathematical	—	`StarModule` `ZeroAtInftyContinuousMap` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instStar` `instSMul`	—	`ext` `StarModule.star_smul`
`instZeroAtInftyContinuousMapClass` 📖	mathematical	—	`ZeroAtInftyContinuousMapClass` `ZeroAtInftyContinuousMap` `instFunLike`	—	`ContinuousMap.continuous_toFun` `zero_at_infty'`
`isBounded_image` 📖	mathematical	—	`Bornology.IsBounded` `PseudoMetricSpace.toBornology` `Set.image` `DFunLike.coe` `ZeroAtInftyContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instFunLike`	—	`Bornology.IsBounded.subset` `isBounded_range` `Set.image_subset_range`
`isBounded_range` 📖	mathematical	—	`Bornology.IsBounded` `PseudoMetricSpace.toBornology` `Set.range` `DFunLike.coe` `ZeroAtInftyContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instFunLike`	—	`Metric.isBounded_range_iff` `bounded` `instZeroAtInftyContinuousMapClass`
`isClosed_range_toBCF` 📖	mathematical	—	`IsClosed` `BoundedContinuousFunction` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `BoundedContinuousFunction.instPseudoMetricSpace` `Set.range` `ZeroAtInftyContinuousMap` `toBCF`	—	`isClosed_iff_clusterPt` `Metric.tendsto_nhds` `Nat.instAtLeastTwoHAddOfNat` `clusterPt_principal_iff` `Metric.ball_mem_nhds` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Filter.Eventually.mp` `ZeroAtInftyContinuousMapClass.zero_at_infty` `instZeroAtInftyContinuousMapClass` `Filter.Eventually.of_forall` `dist_triangle_left` `add_lt_add_of_le_of_lt` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `BoundedContinuousFunction.dist_coe_le_dist` `le_imp_le_of_le_of_le` `add_le_add_left` `le_of_lt` `Metric.mem_ball` `le_refl` `add_halves` `CharZero.NeZero.two` `IsStrictOrderedRing.toCharZero`
`isometry_toBCF` 📖	mathematical	—	`Isometry` `ZeroAtInftyContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `BoundedContinuousFunction` `PseudoMetricSpace.toPseudoEMetricSpace` `instPseudoMetricSpace` `BoundedContinuousFunction.instPseudoMetricSpace` `toBCF`	—	—
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `ZeroAtInftyContinuousMap` `MulZeroClass.toZero` `instFunLike` `instMul` `MulZeroClass.toMul`	—	—
`neg_apply` 📖	mathematical	—	`DFunLike.coe` `ZeroAtInftyContinuousMap` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `instFunLike` `instNeg` `NegZeroClass.toNeg`	—	—
`norm_toBCF_eq_norm` 📖	mathematical	—	`Norm.norm` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `BoundedContinuousFunction.instNorm` `toBCF` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `ZeroAtInftyContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toNorm` `instSeminormedAddCommGroup`	—	—
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `ZeroAtInftyContinuousMap` `instFunLike` `instSMul` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass`	—	—
`star_apply` 📖	mathematical	—	`DFunLike.coe` `ZeroAtInftyContinuousMap` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instFunLike` `Star.star` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar`	—	—
`sub_apply` 📖	mathematical	—	`DFunLike.coe` `ZeroAtInftyContinuousMap` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `instFunLike` `instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	—
`tendsto_iff_tendstoUniformly` 📖	mathematical	—	`Filter.Tendsto` `ZeroAtInftyContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `nhds` `instPseudoMetricSpace` `TendstoUniformly` `DFunLike.coe` `instFunLike`	—	`BoundedContinuousFunction.tendsto_iff_tendstoUniformly`
`toBCF_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `BoundedContinuousFunction.instFunLike` `toBCF` `ZeroAtInftyContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instFunLike`	—	—
`toBCF_injective` 📖	mathematical	—	`ZeroAtInftyContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `BoundedContinuousFunction` `toBCF`	—	`ext` `DFunLike.congr_fun`
`uniformContinuous` 📖	mathematical	—	`UniformContinuous` `DFunLike.coe`	—	`Continuous.uniformContinuous_of_tendsto_cocompact` `ContinuousMapClass.map_continuous` `ZeroAtInftyContinuousMapClass.toContinuousMapClass` `ZeroAtInftyContinuousMapClass.zero_at_infty`
`zero_apply` 📖	mathematical	—	`DFunLike.coe` `ZeroAtInftyContinuousMap` `instFunLike` `instZero`	—	—
`zero_at_infty'` 📖	mathematical	—	`Filter.Tendsto` `ContinuousMap.toFun` `toContinuousMap` `Filter.cocompact` `nhds`	—	—
`zero_comp` 📖	mathematical	—	`comp` `ZeroAtInftyContinuousMap` `instZero`	—	—

ZeroAtInftyContinuousMap.ContinuousMap

Definitions

Name	Category	Theorems
`liftZeroAtInfty` 📖	CompOp	2 math math: `liftZeroAtInfty_apply_toFun`, `liftZeroAtInfty_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`liftZeroAtInfty_apply_toFun` 📖	mathematical	—	`DFunLike.coe` `ZeroAtInftyContinuousMap` `ZeroAtInftyContinuousMap.instFunLike` `Equiv` `ContinuousMap` `EquivLike.toFunLike` `Equiv.instEquivLike` `liftZeroAtInfty` `ContinuousMap.instFunLike`	—	—
`liftZeroAtInfty_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `ZeroAtInftyContinuousMap` `ContinuousMap` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `liftZeroAtInfty` `toContinuousMap` `ZeroAtInftyContinuousMap.instFunLike`	—	—

ZeroAtInftyContinuousMap.zeroAtInftyContinuousMapClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofCompact` 📖	mathematical	—	`ZeroAtInftyContinuousMapClass`	—	`Filter.cocompact_eq_bot`

ZeroAtInftyContinuousMapClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toContinuousMapClass` 📖	mathematical	—	`ContinuousMapClass`	—	—
`zero_at_infty` 📖	mathematical	—	`Filter.Tendsto` `DFunLike.coe` `Filter.cocompact` `nhds`	—	—

(root)

Definitions

Name	Category	Theorems
`ZeroAtInftyContinuousMap` 📖	CompData	42 math math: `ZeroAtInftyContinuousMap.toBCF_injective`, `ZeroAtInftyContinuousMap.instIsCentralScalar`, `ZeroAtInftyContinuousMap.add_apply`, `ZeroAtInftyContinuousMap.coe_smul`, `ZeroAtInftyContinuousMap.instIsScalarTower`, `ZeroAtInftyContinuousMap.smul_apply`, `ZeroAtInftyContinuousMap.coe_mk`, `ZeroAtInftyContinuousMap.coe_comp_to_continuous_fun`, `ZeroAtInftyContinuousMap.instNormedStarGroup`, `ZeroAtInftyContinuousMap.isClosed_range_toBCF`, `ZeroAtInftyContinuousMap.dist_toBCF_eq_dist`, `ZeroAtInftyContinuousMap.coe_zero`, `ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty_apply_toFun`, `ZeroAtInftyContinuousMap.zero_apply`, `ZeroAtInftyContinuousMap.toBCF_apply`, `ZeroAtInftyContinuousMap.neg_apply`, `ZeroAtInftyContinuousMap.sub_apply`, `ZeroAtInftyContinuousMap.instZeroAtInftyContinuousMapClass`, `ZeroAtInftyContinuousMap.isBounded_image`, `ZeroAtInftyContinuousMap.coe_mul`, `ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty_symm_apply`, `ZeroAtInftyContinuousMap.instCompleteSpace`, `ZeroAtInftyContinuousMap.norm_toBCF_eq_norm`, `ZeroAtInftyContinuousMap.instCStarRing`, `ZeroAtInftyContinuousMap.instSMulCommClass`, `ZeroAtInftyContinuousMap.instStarModule`, `ZeroAtInftyContinuousMap.zero_comp`, `ZeroAtInftyContinuousMap.ext_iff`, `ZeroAtInftyContinuousMap.isometry_toBCF`, `ZeroAtInftyContinuousMap.coe_toContinuousMap`, `PadicInt.mahlerEquiv_apply`, `ZeroAtInftyContinuousMap.star_apply`, `ZeroAtInftyContinuousMap.isBounded_range`, `ZeroAtInftyContinuousMap.tendsto_iff_tendstoUniformly`, `PadicInt.mahlerEquiv_symm_apply`, `ZeroAtInftyContinuousMap.coe_sub`, `ZeroAtInftyContinuousMap.coe_add`, `SchwartzMap.toZeroAtInfty_apply`, `ZeroAtInftyContinuousMap.coe_neg`, `ZeroAtInftyContinuousMap.mul_apply`, `SchwartzMap.toZeroAtInftyCLM_apply`, `ZeroAtInftyContinuousMap.coe_star`
`ZeroAtInftyContinuousMapClass` 📖	CompData	4 math math: `CompactlySupportedContinuousMapClass.instZeroAtInftyContinuousMapClass`, `ZeroAtInftyContinuousMap.instZeroAtInftyContinuousMapClass`, `SchwartzMap.instZeroAtInftyContinuousMapClass`, `ZeroAtInftyContinuousMap.zeroAtInftyContinuousMapClass.ofCompact`

---

← Back to Index