(path) connected components are a partition

Stream: Is there code for X?

[Snir Broshi]

import Mathlib
variable (α : Type*) [TopologicalSpace α]

theorem isPartition_connectedComponent :
    Setoid.IsPartition (α := α) <| .range connectedComponent := by
  sorry

theorem isPartition_pathComponent :
    Setoid.IsPartition (α := α) <| .range pathComponent := by
  sorry

[Edward van de Meent]

i don't think something like this is in mathlib... but here's my attempt (not mathlib quality):

import Mathlib
variable (α : Type*) [TopologicalSpace α]

lemma Setoid.isPartition_range_of_mem_apply_of_pairwise_disjoint {α : Type*} (f : α → Set α)
  (hmem_self : ∀ x, x ∈ f x) (hdisjoint : ∀ x y, f x ≠ f y → Disjoint (f x) (f y)) :
    Setoid.IsPartition (α := α) <| .range f := by
  refine Set.PairwiseDisjoint.isPartition_of_exists_of_ne_empty ?_ ?_ ?_
  · simp only [Set.PairwiseDisjoint, Set.Pairwise, Set.mem_range, ne_eq, Function.onFun, id_eq, forall_exists_index,
      forall_apply_eq_imp_iff]
    exact hdisjoint
  · intro x
    simp only [Set.mem_range, exists_exists_eq_and]
    use x, hmem_self x
  · simp only [Set.mem_range, Set.ext_iff, Set.mem_empty_iff_false, iff_false, not_exists,
      not_forall, not_not]
    intro x
    use x, hmem_self x

theorem isPartition_connectedComponent :
    Setoid.IsPartition (α := α) <| .range connectedComponent :=
  Setoid.isPartition_range_of_mem_apply_of_pairwise_disjoint connectedComponent
    (fun _ => mem_connectedComponent) (fun _ _ => connectedComponent_disjoint)

variable {α} in
lemma pathComponent_disjoint {x y : α} : pathComponent x ≠ pathComponent y → Disjoint (pathComponent x) (pathComponent y) := by
  rw [Set.disjoint_iff_forall_ne]
  rintro heq a ha b hb rfl
  apply heq
  rw [← pathComponent_congr ha, pathComponent_congr hb]


theorem isPartition_pathComponent :
    Setoid.IsPartition (α := α) <| .range pathComponent :=
  Setoid.isPartition_range_of_mem_apply_of_pairwise_disjoint pathComponent
    (mem_pathComponent_self) (fun _ _ => pathComponent_disjoint)

(really it should be called Set.IsPartition imo, but that's neither here nor there)