Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-04 22:36 fab61c9f

View on Github →

chore(topology/continuous_function/bounded): add simple lemmas (#10149)

Estimated changes

Modified src/topology/continuous_function/bounded.lean

added theorem bounded_continuous_function.add_comp_continuous

added theorem bounded_continuous_function.coe_to_continuous_fun

added theorem bounded_continuous_function.continuous_comp_continuous

added theorem bounded_continuous_function.eq_of_empty

added theorem bounded_continuous_function.lipschitz_comp_continuous

added theorem bounded_continuous_function.zero_comp_continuous