Mathlib Changelog
v4
Changelog
About
Github
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