Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-18 09:32 dab2ae38

View on Github →

feat(category_theory/is_connected): transfer across equivalence (#5021) Also renames some universes to match usual conventions

Estimated changes

Modified src/category_theory/is_connected.lean

modified theorem category_theory.constant_of_preserves_morphisms

added theorem category_theory.is_connected_of_equivalent

added theorem category_theory.is_preconnected_of_equivalent

modified def category_theory.iso_constant