Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-08 10:21 f3dbe9f0

View on Github →

feat(bounded_continuous_function): coe_sum (#6522)

Estimated changes

Modified src/topology/bounded_continuous_function.lean

added def bounded_continuous_function.coe_fn_add_hom

added theorem bounded_continuous_function.coe_sum

modified theorem bounded_continuous_function.coe_zero

added theorem bounded_continuous_function.sum_apply