Canonical way of proving connectedness?

Stream: new members

[Ruth Plümer]

Hello everyone,
I'm working on my first Lean project and have been stuck with one issue: during my proof, I am trying to show that a certain topological space X is connected. I know how to prove it on paper by showing that X is nonempty and the only subsets of X that are clopen are X itself (i.e. univ) and the emptyset.
Now, the explanation for the class ConnectedSpace reads "A connected space is a nonempty one where there is no non-trivial open partition". However, I'm struggling to understand how I should prove

isPreconnected_univ : IsPreconnected (univ : Set X)

I tried searching mathlib for lemmas characterizing IsPreconnected, IsConnected, ConnectedSpace, PreconnectedSpace and connectedComponent and I found none mentioning clopen sets or partitions of open sets. Basically, all lemmas I could find only characterized one of the terms above in terms of the other ones. Is the standard topological definition really not implemented or did I fail to search correctly? And if it's not implemented, what would be the standard way to prove that a given space if connected / preconnected in Lean?

(I'm sorry if this belongs to another channel, I'm new here)

[Aaron Liu]

@loogle ConnectedSpace, IsClopen

[loogle]

:shrug: nothing found

[Aaron Liu]

@loogle |- ConnectedSpace _

[loogle]

:search: IrreducibleSpace.connectedSpace, ConnectedSpace.mk, and 9 more

[Aaron Liu]

@loogle IsConnected, IsClopen

[loogle]

:search: IsLocallyConstant.of_constant_on_connected_clopens

[Aaron Liu]

Do we not have this?

import Mathlib.Topology.Connected.Clopen

variable {X : Type*} [TopologicalSpace X]

theorem preconnectedSpace_iff_clopen :
    PreconnectedSpace X ↔ ∀ s : Set X, IsClopen s → s = ∅ ∨ s = Set.univ :=
  ⟨fun _ s hs ↦ isClopen_iff.mp hs, fun h ↦ ⟨fun u v hu hv huv huu hvv ↦ by
    apply Set.nonempty_iff_ne_empty.mpr
    intro hdj
    have h : uᶜ = v := by
      apply subset_antisymm
      · apply Set.compl_subset_iff_union.mpr
        exact Set.eq_univ_of_univ_subset huv
      · apply Disjoint.subset_compl_left
        apply Set.disjoint_iff_inter_eq_empty.mpr
        rwa [Set.univ_inter] at hdj
    subst h
    obtain rfl | rfl := h u ⟨⟨hv⟩, hu⟩
    · simp at huu
    · simp at hvv⟩⟩

theorem connectedSpace_iff_clopen :
    ConnectedSpace X ↔ Nonempty X ∧ ∀ s : Set X, IsClopen s → s = ∅ ∨ s = Set.univ := by
  rw [connectedSpace_iff_univ, IsConnected /- is this intended? -/, ← preconnectedSpace_iff_univ,
    preconnectedSpace_iff_clopen, Set.nonempty_iff_univ_nonempty]

[Ruben Van de Velde]

Seems worth adding