Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-21 15:22 473bb7d4

View on Github →

feat(topology/locally_constant): basics on locally constant functions (#6192) From lean-liquid

Estimated changes

Modified src/data/set/basic.lean

added theorem set.not_nonempty_empty

Created src/topology/locally_constant/algebra.lean

added theorem locally_constant.div_apply

added theorem locally_constant.inv_apply

added theorem locally_constant.mul_apply

added theorem locally_constant.one_apply

Created src/topology/locally_constant/basic.lean

added theorem is_locally_constant.apply_eq_of_is_preconnected

added theorem is_locally_constant.comp

added theorem is_locally_constant.comp_continuous

added theorem is_locally_constant.comp₂

added theorem is_locally_constant.const

added theorem is_locally_constant.div

added theorem is_locally_constant.exists_open

added theorem is_locally_constant.iff_continuous

added theorem is_locally_constant.iff_continuous_bot

added theorem is_locally_constant.iff_eventually_eq

added theorem is_locally_constant.iff_exists_open

added theorem is_locally_constant.iff_is_const

added theorem is_locally_constant.inv

added theorem is_locally_constant.is_open_fiber

added theorem is_locally_constant.mul

added theorem is_locally_constant.of_constant

added theorem is_locally_constant.of_discrete

added theorem is_locally_constant.one

added theorem is_locally_constant.prod_mk

added theorem is_locally_constant.range_finite

added def is_locally_constant

added theorem locally_constant.apply_eq_of_is_preconnected

added theorem locally_constant.apply_eq_of_preconnected_space

added theorem locally_constant.coe_comap

added theorem locally_constant.coe_inj

added theorem locally_constant.coe_injective

added theorem locally_constant.coe_mk

added def locally_constant.comap

added theorem locally_constant.comap_comp

added theorem locally_constant.comap_const

added theorem locally_constant.comap_id

added theorem locally_constant.congr_arg

added theorem locally_constant.congr_fun

added def locally_constant.const

added theorem locally_constant.eq_const

added theorem locally_constant.exists_eq_const

added theorem locally_constant.ext

added theorem locally_constant.ext_iff

added def locally_constant.map

added theorem locally_constant.map_apply

added theorem locally_constant.map_comp

added theorem locally_constant.map_id

added theorem locally_constant.range_finite

added theorem locally_constant.to_fun_eq_coe

added structure locally_constant