feat: port CategoryTheory.IsConnected (#2443)

Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: Matthew Ballard <matt@mrb.email>
leanprover-community · Mar 11, 2023 · 2207652 · 2207652
1 parent e112ddd
commit 2207652
Show file tree

Hide file tree

Showing 2 changed files with 396 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -304,6 +304,7 @@ import Mathlib.CategoryTheory.Functor.InvIsos
 import Mathlib.CategoryTheory.Functor.ReflectsIso
 import Mathlib.CategoryTheory.Groupoid
 import Mathlib.CategoryTheory.Groupoid.Basic
+import Mathlib.CategoryTheory.IsConnected
 import Mathlib.CategoryTheory.Iso
 import Mathlib.CategoryTheory.IsomorphismClasses
 import Mathlib.CategoryTheory.LiftingProperties.Adjunction