Commit 2023-06-16 17:31 b21a13bb

View on Github →

feat: port Topology.ContinuousFunction.ZeroAtInfty (#4255)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/ContinuousFunction/ZeroAtInfty.lean

added def ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty

added theorem ZeroAtInftyContinuousMap.add_apply

added theorem ZeroAtInftyContinuousMap.bounded_image

added theorem ZeroAtInftyContinuousMap.bounded_range

added theorem ZeroAtInftyContinuousMap.closed_range_toBcf

added theorem ZeroAtInftyContinuousMap.coe_add

added theorem ZeroAtInftyContinuousMap.coe_comp_to_continuous_fun

added theorem ZeroAtInftyContinuousMap.coe_copy

added theorem ZeroAtInftyContinuousMap.coe_mul

added theorem ZeroAtInftyContinuousMap.coe_neg

added theorem ZeroAtInftyContinuousMap.coe_nsmulRec

added theorem ZeroAtInftyContinuousMap.coe_smul

added theorem ZeroAtInftyContinuousMap.coe_star

added theorem ZeroAtInftyContinuousMap.coe_sub

added theorem ZeroAtInftyContinuousMap.coe_toContinuousMap

added theorem ZeroAtInftyContinuousMap.coe_zero

added theorem ZeroAtInftyContinuousMap.coe_zsmulRec

added def ZeroAtInftyContinuousMap.comp

added def ZeroAtInftyContinuousMap.compAddMonoidHom

added def ZeroAtInftyContinuousMap.compLinearMap

added def ZeroAtInftyContinuousMap.compMulHom

added def ZeroAtInftyContinuousMap.compNonUnitalAlgHom

added theorem ZeroAtInftyContinuousMap.comp_assoc

added theorem ZeroAtInftyContinuousMap.comp_id

added theorem ZeroAtInftyContinuousMap.copy_eq

added theorem ZeroAtInftyContinuousMap.dist_toBcf_eq_dist

added theorem ZeroAtInftyContinuousMap.eq_of_empty

added theorem ZeroAtInftyContinuousMap.ext

added theorem ZeroAtInftyContinuousMap.isometry_toBcf

added theorem ZeroAtInftyContinuousMap.mul_apply

added theorem ZeroAtInftyContinuousMap.neg_apply

added theorem ZeroAtInftyContinuousMap.norm_toBcf_eq_norm

added theorem ZeroAtInftyContinuousMap.smul_apply

added theorem ZeroAtInftyContinuousMap.star_apply

added theorem ZeroAtInftyContinuousMap.sub_apply

added theorem ZeroAtInftyContinuousMap.tendsto_iff_tendstoUniformly

added def ZeroAtInftyContinuousMap.toBcf

added theorem ZeroAtInftyContinuousMap.toBcf_injective

added theorem ZeroAtInftyContinuousMap.uniformContinuous

added def ZeroAtInftyContinuousMap.zeroAtInftyContinuousMapClass.ofCompact

added theorem ZeroAtInftyContinuousMap.zero_apply

added theorem ZeroAtInftyContinuousMap.zero_comp

added structure ZeroAtInftyContinuousMap