Commit 2023-03-07 06:34 c3484b5d

View on Github →

feat: port Topology.Instances.NNReal (#2672)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/ContinuousFunction/Basic.lean

added def ContinuousMap.Simps.apply

Created Mathlib/Topology/Instances/NNReal.lean

added def ContinuousMap.coeNNRealReal

added theorem NNReal.coe_tsum

added theorem NNReal.coe_tsum_of_nonneg

added theorem NNReal.comap_coe_atTop

added theorem NNReal.continuous_coe

added theorem NNReal.hasSum_coe

added theorem NNReal.hasSum_real_toNNReal_of_nonneg

added theorem NNReal.infᵢ_real_pos_eq_infᵢ_nNReal_pos

added theorem NNReal.map_coe_atTop

added theorem NNReal.nhds_zero

added theorem NNReal.nhds_zero_basis

added def NNReal.powOrderIso

added theorem NNReal.summable_coe

added theorem NNReal.summable_comp_injective

added theorem NNReal.summable_mk

added theorem NNReal.summable_nat_add

added theorem NNReal.tendsto_atTop_zero_of_summable

added theorem NNReal.tendsto_coe'

added theorem NNReal.tendsto_coe

added theorem NNReal.tendsto_coe_atTop

added theorem NNReal.tendsto_cofinite_zero_of_summable

added theorem continuous_real_toNNReal

added theorem tendsto_real_toNNReal

added theorem tendsto_real_toNNReal_atTop