Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-23 13:11 2ec6de7d

View on Github →

feat(topology/connected): sufficient conditions for the preimage of a connected set to be connected (#10289) and other simple connectedness results

Estimated changes

Modified src/data/set/basic.lean

added theorem set.nonempty.preimage'

Modified src/data/set/lattice.lean

added theorem disjoint.subset_left_of_subset_union

added theorem disjoint.subset_right_of_subset_union

Modified src/topology/connected.lean

added theorem is_connected.preimage_of_closed_map

added theorem is_connected.preimage_of_open_map

added theorem is_preconnected.preimage_of_closed_map

added theorem is_preconnected.preimage_of_open_map

added theorem is_preconnected.subset_left_of_subset_union

added theorem is_preconnected.subset_or_subset

added theorem is_preconnected.subset_right_of_subset_union