Commit 2023-02-02 04:56 94459ebe

View on Github →

feat: port Topology.Connected (#1934)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Connected.lean

added theorem ConnectedComponents.coe_eq_coe'

added theorem ConnectedComponents.coe_eq_coe

added theorem ConnectedComponents.coe_ne_coe

added theorem ConnectedComponents.continuous_coe

added def ConnectedComponents.mk

added theorem ConnectedComponents.quotientMap_coe

added theorem ConnectedComponents.range_coe

added theorem ConnectedComponents.surjective_coe

added def ConnectedComponents

added def Continuous.connectedComponentsLift

added theorem Continuous.connectedComponentsLift_apply_coe

added theorem Continuous.connectedComponentsLift_comp_coe

added theorem Continuous.connectedComponentsLift_continuous

added theorem Continuous.connectedComponentsLift_unique

added def Continuous.connectedComponentsMap

added theorem Continuous.connectedComponentsMap_continuous

added theorem Continuous.image_connectedComponent_eq_singleton

added theorem Continuous.image_connectedComponent_subset

added theorem Continuous.image_eq_of_connectedComponent_eq

added theorem Continuous.mapsTo_connectedComponent

added theorem DenseRange.preconnectedSpace

added theorem Embedding.isTotallyDisconnected

added theorem Inducing.isPreconnected_image

added theorem IsClopen.bunionᵢ_connectedComponent_eq

added theorem IsClopen.connectedComponent_subset

added theorem IsClopen.eq_univ

added theorem IsConnected.bunionᵢ_of_chain

added theorem IsConnected.bunionᵢ_of_reflTransGen

added theorem IsConnected.isPreconnected

added theorem IsConnected.nonempty

added theorem IsConnected.preimage_of_closedMap

added theorem IsConnected.preimage_of_openMap

added theorem IsConnected.prod

added theorem IsConnected.subset_connectedComponent

added theorem IsConnected.union

added theorem IsConnected.unionᵢ_of_chain

added theorem IsConnected.unionᵢ_of_reflTransGen

added def IsConnected

added theorem IsIrreducible.isConnected

added theorem IsPreconnected.bunionᵢ_of_chain

added theorem IsPreconnected.bunionᵢ_of_reflTransGen

added theorem IsPreconnected.connectedComponentIn

added theorem IsPreconnected.constant

added theorem IsPreconnected.constant_of_mapsTo

added theorem IsPreconnected.preimage_of_closed_map

added theorem IsPreconnected.preimage_of_open_map

added theorem IsPreconnected.prod

added theorem IsPreconnected.subset_clopen

added theorem IsPreconnected.subset_connectedComponent

added theorem IsPreconnected.subset_connectedComponentIn

added theorem IsPreconnected.subset_left_of_subset_union

added theorem IsPreconnected.subset_of_closure_inter_subset

added theorem IsPreconnected.subset_or_subset

added theorem IsPreconnected.subset_right_of_subset_union

added theorem IsPreconnected.subsingleton

added theorem IsPreconnected.union'

added theorem IsPreconnected.union

added theorem IsPreconnected.unionᵢ_of_chain

added theorem IsPreconnected.unionᵢ_of_reflTransGen

added theorem IsPreconnected.unionₛ_directed

added def IsPreconnected

added theorem IsPreirreducible.isPreconnected

added def IsTotallyDisconnected

added def IsTotallySeparated

added theorem PreconnectedSpace.connectedComponent_eq_univ

added theorem PreconnectedSpace.constant

added theorem QuotientMap.image_connectedComponent

added theorem QuotientMap.preimage_connectedComponent

added theorem Set.Subsingleton.isPreconnected

added theorem Sigma.isConnected_iff

added theorem Sigma.isPreconnected_iff

added theorem Subtype.connectedSpace

added theorem Subtype.preconnectedSpace

added theorem Sum.isConnected_iff

added theorem Sum.isPreconnected_iff

added def connectedComponent

added def connectedComponentIn

added theorem connectedComponentIn_eq

added theorem connectedComponentIn_eq_empty

added theorem connectedComponentIn_eq_image

added theorem connectedComponentIn_mem_nhds

added theorem connectedComponentIn_mono

added theorem connectedComponentIn_nonempty_iff

added theorem connectedComponentIn_subset

added theorem connectedComponentIn_univ

added def connectedComponentSetoid

added theorem connectedComponent_disjoint

added theorem connectedComponent_eq

added theorem connectedComponent_nonempty

added theorem connectedComponent_subset_interᵢ_clopen

added theorem connectedComponents_lift_unique'

added theorem connectedComponents_preimage_image

added theorem connectedComponents_preimage_singleton

added theorem connectedSpace_iff_connectedComponent

added theorem disjoint_or_subset_of_clopen

added theorem exists_clopen_of_totally_separated

added theorem frontier_eq_empty_iff

added theorem irreducibleComponent_subset_connectedComponent

added theorem isClopen_connectedComponent

added theorem isClopen_iff

added theorem isClosed_connectedComponent

added theorem isConnected_connectedComponent

added theorem isConnected_connectedComponentIn_iff

added theorem isConnected_iff_connectedSpace

added theorem isConnected_iff_unionₛ_disjoint_open

added theorem isConnected_range

added theorem isConnected_singleton

added theorem isConnected_univ

added theorem isConnected_univ_pi

added theorem isOpen_connectedComponent

added theorem isPreconnected_closed_iff

added theorem isPreconnected_connectedComponent

added theorem isPreconnected_connectedComponentIn

added theorem isPreconnected_empty

added theorem isPreconnected_iff_preconnectedSpace

added theorem isPreconnected_iff_subset_of_disjoint

added theorem isPreconnected_iff_subset_of_disjoint_closed

added theorem isPreconnected_iff_subset_of_fully_disjoint_closed

added theorem isPreconnected_of_forall

added theorem isPreconnected_of_forall_constant

added theorem isPreconnected_of_forall_pair

added theorem isPreconnected_range

added theorem isPreconnected_singleton

added theorem isPreconnected_unionᵢ

added theorem isPreconnected_unionₛ

added theorem isPreconnected_univ_pi

added theorem isTotallyDisconnected_empty

added theorem isTotallyDisconnected_of_clopen_set

added theorem isTotallyDisconnected_of_image

added theorem isTotallyDisconnected_of_isTotallySeparated

added theorem isTotallyDisconnected_of_totallyDisconnectedSpace

added theorem isTotallyDisconnected_singleton

added theorem isTotallySeparated_empty

added theorem isTotallySeparated_singleton

added theorem locallyConnectedSpace_iff_connectedComponentIn_open

added theorem locallyConnectedSpace_iff_connected_basis

added theorem locallyConnectedSpace_iff_connected_subsets

added theorem locallyConnectedSpace_iff_open_connected_basis

added theorem locallyConnectedSpace_iff_open_connected_subsets

added theorem locallyConnectedSpace_of_connected_bases

added theorem mem_connectedComponent

added theorem mem_connectedComponentIn

added theorem nonempty_frontier_iff

added theorem nonempty_inter

added theorem preconnectedSpace_iff_connectedComponent

added theorem preconnectedSpace_of_forall_constant

added theorem preimage_connectedComponent_connected

added theorem totallyDisconnectedSpace_iff_connectedComponent_singleton

added theorem totallyDisconnectedSpace_iff_connectedComponent_subsingleton

Modified Mathlib/Topology/ContinuousOn.lean

added theorem ContinuousOn.restrict_mapsTo

Modified Mathlib/Topology/SubsetProperties.lean

deleted theorem clopen_range_sigmaMk

added theorem isClopen_range_inl

added theorem isClopen_range_inr

added theorem isClopen_range_sigmaMk