Overloading dot notation

Stream: mathlib4

[Steven Clontz]

Working to port all SeparatedNhds to use disjoint filters, I have theorems written like this:

theorem Disjoint.disjointOpenNhds {s t : Set X} (dis : Disjoint (𝓝ˢ s) (𝓝ˢ t)) :
    ∃ u v, IsOpen u ∧ s ⊆ u ∧ IsOpen v ∧ t ⊆ v ∧ Disjoint u v :=
  sorry

theorem Disjoint.disjointOpenNhds' {x y : X} (dis : Disjoint (𝓝 x) (𝓝 y)) :
    ∃ u v, IsOpen u ∧ x ∈ u ∧ IsOpen v ∧ y ∈ v ∧ Disjoint u v :=
  sorry

Which would provide a convenient way to obtain the "right" open neighborhoods by calling disSets.disjointOpennhds where disSets : Disjoint (𝓝ˢ s) (𝓝ˢ t), and calling disPts.disjointOpennhds' where disPts : Disjoint (𝓝 s) (𝓝 y).

My question: is there a way to make both methods be simply .disjointOpenNhds?

[Eric Wieser]

I don't think so, but also the first one is about docs#nhdsSet not docs#nhds so should be named differently anyway

[Steven Clontz]

Sounds reasonable, perhaps

theorem Disjoint.disjointOpenNhdsSet {s t : Set X} (dis : Disjoint (𝓝ˢ s) (𝓝ˢ t)) :
    ∃ u v, IsOpen u ∧ s ⊆ u ∧ IsOpen v ∧ t ⊆ v ∧ Disjoint u v :=
  sorry

theorem Disjoint.disjointOpenNhds {x y : X} (dis : Disjoint (𝓝 x) (𝓝 y)) :
    ∃ u v, IsOpen u ∧ x ∈ u ∧ IsOpen v ∧ y ∈ v ∧ Disjoint u v :=
  sorry

and I guess (?)

theorem Disjoint.disjointOpenNhdNhdSet {x : X} {t : Set X} (dis : Disjoint (𝓝 x) (𝓝ˢ t)) :
    ∃ u v, IsOpen u ∧ x ∈ u ∧ IsOpen v ∧ t ⊆ v ∧ Disjoint u v :=
  sorry

theorem Disjoint.disjointOpenNhdSetNhd {s : Set X} {y : X} (dis : Disjoint (𝓝ˢ s) (𝓝 y) ) :
    ∃ u v, IsOpen u ∧ s ⊆ u ∧ IsOpen v ∧ y ∈ v ∧ Disjoint u v :=
  sorry

[Eric Wieser]

Note the naming convention for theorems is snake_case

[Steven Clontz]

then perhaps Disjoint.disjoint_open_nhdsSet, Disjoint.disjoint_open_nhds, Disjoint.disjoint_open_nhd_nhdSet, and Disjoint.disjoint_open_nhdSet_nhd