connected_space.is_connected_univ

Stream: Is there code for X?

[Nicolò Cavalleri]

Is this really not in mathlib?

lemma connected_space.is_connected_univ {α : Type*} [topological_space α] [connected_space α] :
  is_connected (univ : set α) := ⟨univ_nonempty, is_preconnected_univ⟩

[Adam Topaz]

It should be called docs#is_connected_univ I would guess...

[Nicolò Cavalleri]

Shouldn't it be called as in the title with that namespace?

[Adam Topaz]

We have things like docs#compact_univ

[Adam Topaz]

I think the naming here should follow the same convention