Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-09 11:06 656ef0a5

View on Github →

chore(topology/instances/nnreal): use notation (#4548)

Estimated changes

Modified src/topology/instances/nnreal.lean

modified theorem nnreal.coe_tsum

modified theorem nnreal.continuous.sub

modified theorem nnreal.continuous_coe

modified theorem nnreal.continuous_sub

modified theorem nnreal.has_sum_coe

modified theorem nnreal.sum_add_tsum_nat_add

modified theorem nnreal.summable_comp_injective

modified theorem nnreal.summable_nat_add

modified theorem nnreal.tendsto.sub

modified theorem nnreal.tendsto_coe