Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-23 22:06 0ca85a74

View on Github →

feat(data/set/basic, topology/{subset_properties, connected}): A space is preconnected iff every continuous map to a discrete space is constant (#17070) This useful characterisation was missing from mathlib.

Estimated changes

Modified src/data/set/basic.lean

added theorem set.mem_iff_bool_indicator

added theorem set.not_mem_iff_bool_indicator

added theorem set.preimage_bool_indicator

added theorem set.preimage_bool_indicator_eq_union

added theorem set.preimage_bool_indicator_ff

added theorem set.preimage_bool_indicator_tt

added theorem set.preimage_subtype_coe_eq_compl

Modified src/topology/connected.lean

added theorem is_preconnected.constant

added theorem is_preconnected_of_forall_constant

added theorem preconnected_space.constant

added theorem preconnected_space_of_forall_constant

Modified src/topology/subset_properties.lean

added theorem continuous_bool_indicator_iff_clopen

added theorem continuous_on_indicator_iff_clopen