Commit 2023-02-07 20:20 3d72b547

View on Github →

feat: port Topology.LocallyConstant.Basic (#2141)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/LocallyConstant/Basic.lean

added theorem IsLocallyConstant.apply_eq_of_isPreconnected

added theorem IsLocallyConstant.apply_eq_of_preconnectedSpace

added theorem IsLocallyConstant.comp_continuous

added theorem IsLocallyConstant.comp₂

added theorem IsLocallyConstant.desc

added theorem IsLocallyConstant.div

added theorem IsLocallyConstant.eq_const

added theorem IsLocallyConstant.exists_eq_const

added theorem IsLocallyConstant.exists_open

added theorem IsLocallyConstant.iff_continuous

added theorem IsLocallyConstant.iff_eventually_eq

added theorem IsLocallyConstant.iff_exists_open

added theorem IsLocallyConstant.iff_isOpen_fiber

added theorem IsLocallyConstant.iff_isOpen_fiber_apply

added theorem IsLocallyConstant.iff_is_const

added theorem IsLocallyConstant.inv

added theorem IsLocallyConstant.isClopen_fiber

added theorem IsLocallyConstant.isClosed_fiber

added theorem IsLocallyConstant.isOpen_fiber

added theorem IsLocallyConstant.mul

added theorem IsLocallyConstant.of_constant

added theorem IsLocallyConstant.of_constant_on_connected_components

added theorem IsLocallyConstant.of_constant_on_preconnected_clopens

added theorem IsLocallyConstant.of_discrete

added theorem IsLocallyConstant.one

added theorem IsLocallyConstant.prod_mk

added theorem IsLocallyConstant.range_finite

added def IsLocallyConstant

added def LocallyConstant.Simps.apply

added theorem LocallyConstant.apply_eq_of_isPreconnected

added theorem LocallyConstant.apply_eq_of_preconnectedSpace

added theorem LocallyConstant.coe_comap

added theorem LocallyConstant.coe_const

added theorem LocallyConstant.coe_continuousMap

added theorem LocallyConstant.coe_desc

added theorem LocallyConstant.coe_inj

added theorem LocallyConstant.coe_injective

added theorem LocallyConstant.coe_mk

added theorem LocallyConstant.comap_comp

added theorem LocallyConstant.comap_const

added theorem LocallyConstant.comap_id

added theorem LocallyConstant.congr_arg

added theorem LocallyConstant.congr_fun

added def LocallyConstant.const

added def LocallyConstant.desc

added theorem LocallyConstant.eq_const

added theorem LocallyConstant.exists_eq_const

added theorem LocallyConstant.ext

added theorem LocallyConstant.ext_iff

added def LocallyConstant.flip

added theorem LocallyConstant.flip_unflip

added theorem LocallyConstant.locallyConstant_eq_of_fiber_zero_eq

added def LocallyConstant.map

added theorem LocallyConstant.map_apply

added theorem LocallyConstant.map_comp

added theorem LocallyConstant.map_id

added theorem LocallyConstant.mulIndicator_apply_eq_if

added theorem LocallyConstant.mulIndicator_of_mem

added theorem LocallyConstant.mulIndicator_of_not_mem

added def LocallyConstant.ofClopen

added theorem LocallyConstant.ofClopen_fiber_one

added theorem LocallyConstant.ofClopen_fiber_zero

added theorem LocallyConstant.range_finite

added def LocallyConstant.toContinuousMap

added theorem LocallyConstant.toContinuousMap_injective

added theorem LocallyConstant.toFun_eq_coe

added def LocallyConstant.unflip

added theorem LocallyConstant.unflip_flip

added structure LocallyConstant