Filtered categories are connected

theorem CategoryTheory.IsFilteredOrEmpty.isPreconnected (C : Type u) [Category.{v, u} C] [IsFilteredOrEmpty C] : IsPreconnected C

theorem CategoryTheory.IsCofilteredOrEmpty.isPreconnected (C : Type u) [Category.{v, u} C] [IsCofilteredOrEmpty C] : IsPreconnected C

theorem CategoryTheory.IsFiltered.isConnected (C : Type u) [Category.{v, u} C] [IsFiltered C] : IsConnected C

theorem CategoryTheory.IsCofiltered.isConnected (C : Type u) [Category.{v, u} C] [IsCofiltered C] : IsConnected C