Typeclass for nontrivial topology

Stream: Is there code for X?

[Eric Wieser]

Do we have something like this?

import Mathlib

variable {α}

class NontrivialTopology (α) [TopologicalSpace α] where
  ne_top : ‹TopologicalSpace α› ≠ ⊤

theorem exists_not_inseparable (α) [TopologicalSpace α] [NontrivialTopology α] :
    ∃ x y : α, ¬ Inseparable x y := by
  have := NontrivialTopology.ne_top (α := α)
  contrapose! this
  ext
  simp_rw [inseparable_iff_forall_isOpen] at this
  simp_rw [isOpen_iff_mem_nhds, nhds_top, Filter.mem_top] at *
  refine ⟨fun h i hi => top_unique ?_, fun h i hi => ?_⟩
  · exact fun x _ ↦ (this x i _ h).2 hi
  · rw [h i hi]
    exact Filter.univ_mem

instance {α} [TopologicalSpace α] [NontrivialTopology α] : Nontrivial (SeparationQuotient α) :=
  let ⟨x, y, hxy⟩ := exists_not_inseparable α
  ⟨⟦x⟧, ⟦y⟧, mt Quotient.exact hxy⟩

[Notification Bot]

2 messages were moved here from #Is there code for X? > Typeclass for indiscrete topology by Eric Wieser.

[Notification Bot]

A message was moved from this topic to #Is there code for X? > Typeclass for indiscrete topology by Eric Wieser.

[Yaël Dillies]

I saw
Eric Wieser said:

we have a few lemmas using ∃ x, ‖x‖ ≠ 0 for seminormed spaces which end up with API duplication for nontrivial normed spaces.

in the original thread. Would a statement about 𝓝 x for some x : α suffice?

[Eric Wieser]

I don't really understand your question, but

theorem exists_norm_ne_zero {α} [SeminormedAddCommGroup α] [NontrivialTopology α] :
    ∃ x : α, ‖x‖ ≠ 0 := by
  obtain ⟨x, y, h⟩ := exists_not_inseparable α
  refine ⟨x - y, mt ?_ h⟩
  rw [← dist_eq_norm, Metric.inseparable_iff]
  exact id

gives me what I need

[Eric Wieser]

My initial goal is generalizing docs#NormedSpace.nonempty_sphere

[Eric Wieser]

Anyway, #28102 adds (much shorter versions of) the proofs in the top post without yet introducing any typeclasses.

[Eric Wieser]

#29120 explores adding new typeclasses and generalizes exists_norm_eq to nontrivial seminormed spaces.