Commit 2021-11-30 13:24 4d90ff97

View on Github →

feat(topology/connected): Connectedness in sum and sigma type (#10511) This provides the compact_space and totally_disconnected_space instances for α ⊕ β and Σ i, π i.

Estimated changes

Modified src/data/set/lattice.lean

added theorem set.sigma.univ

Modified src/topology/connected.lean

modified theorem is_connected_univ_pi

modified theorem is_preconnected_univ_pi

added theorem sigma.is_connected_iff

added theorem sigma.is_preconnected_iff

added theorem sum.is_connected_iff

added theorem sum.is_preconnected_iff

Modified src/topology/constructions.lean

added theorem is_open_sigma_fst_preimage

Modified src/topology/subset_properties.lean

added theorem clopen_range_sigma_mk