Express membership of neighbourhood filter in rel. topology

Stream: new members

[Stephan Maier]

Hi, I am trying to define relations between sets in a topological space. Intziitively, I would write code as follows to express that a set s1 is in the neighbourhood filter of a point p in the relative topology on a subset s2 of the entire space. The code, of coures, does not work, and probably it is wrong in many other ways. But what is the right way to work with relative topology? Thanks for a hint.

def example_nhd
  {X : Type*} [TopologicalSpace X]
  (s1 s2: Set X) (hsub : s1 ⊆ s2)
  (p : X) (hpin1 : p ∈ s1) := s1 ∈ nhds_induced (fun s : s1 => ↑s) ⟨p, hpin1⟩

[Anatole Dedecker]

The idiomatic way to do this would be to use docs#nhdsWithin, which gives the filter of neighborhoods of a point inside a subset.

[Anatole Dedecker]

You can also consider s2 itself as a topological space, and your condition becomes that the preimage by docs#Subtype.val of s1 is a neighborhood of p. Then you can use the usual docs#nhds

[Anatole Dedecker]

But the nhdsWithin approach will probably be easier

[Stephan Maier]

Anatole Dedecker said:

The idiomatic way to do this would be to use docs#nhdsWithin, which gives the filter of neighborhoods of a point inside a subset.

Thanks a lot, that looks like the way to procede! Yours, Stephan