Commit 2020-09-15 12:59 d3a17196

View on Github →

feat(category_theory/is_connected): make is_connected a Prop (#4136) Also renames connected to is_connected, and relies on classical.arbitrary slightly less.

Estimated changes

Renamed src/category_theory/connected.lean to src/category_theory/is_connected.lean

modified theorem category_theory.any_functor_const_on_obj

deleted def category_theory.connected.of_any_functor_const_on_obj

deleted def category_theory.connected.of_constant_of_preserves_morphisms

deleted def category_theory.connected.of_induct

deleted def category_theory.connected_of_zigzag

deleted theorem category_theory.connected_zigzag

modified theorem category_theory.constant_of_preserves_morphisms

deleted def category_theory.discrete_connected_equiv_punit

added def category_theory.discrete_is_connected_equiv_punit

modified theorem category_theory.equiv_relation

modified theorem category_theory.exists_zigzag'

modified theorem category_theory.induct_on_objects

added theorem category_theory.is_connected.of_any_functor_const_on_obj

added theorem category_theory.is_connected.of_constant_of_preserves_morphisms

added theorem category_theory.is_connected.of_induct

added theorem category_theory.is_connected_of_zigzag

added theorem category_theory.is_connected_zigzag

added def category_theory.iso_constant

deleted theorem category_theory.nat_trans_from_connected

added theorem category_theory.nat_trans_from_is_connected

deleted def category_theory.zigzag_connected

added theorem category_theory.zigzag_is_connected

Modified src/category_theory/limits/connected.lean

modified def category_theory.prod_preserves_connected_limits

Modified src/category_theory/limits/shapes/constructions/over/connected.lean

modified def category_theory.over.creates_connected.raise_cone

modified def category_theory.over.creates_connected.raised_cone_is_limit

modified theorem category_theory.over.creates_connected.raised_cone_lowers_to_original