Filtered categories are connected

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

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

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

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