Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-10 08:06 a4ea8895

View on Github →

feat(topology/connected): make connected_component_in more usable, develop API (#15964) From the Sphere Eversion Project

Estimated changes

Modified src/topology/connected.lean

modified def connected_component_in

added theorem connected_component_in_eq

added theorem connected_component_in_eq_empty

added theorem connected_component_in_eq_image

added theorem connected_component_in_mono

added theorem connected_component_in_nonempty_iff

added theorem connected_component_in_subset

added theorem connected_component_in_univ

added theorem connected_component_nonempty

added theorem is_connected_connected_component_in_iff

added theorem is_preconnected.connected_component_in

added theorem is_preconnected.subset_connected_component_in

added theorem is_preconnected_connected_component_in

added theorem mem_connected_component_in