HasBasis.nhds_interior

Stream: Is there code for X?

[Anatole Dedecker]

Do we really not have the following ?

import Mathlib.Topology.Basic

open Filter Topology

variable {ι X : Type*}

lemma Filter.HasBasis.nhds_interior [TopologicalSpace X] {x : X} {s : ι → Set X}
    {p : ι → Prop} (H : HasBasis (𝓝 x) p s) : HasBasis (𝓝 x) p (interior ∘ s) :=
  H.to_subset (fun _ _ ↦ interior_subset) (fun _ h ↦ interior_mem_nhds.mpr <| H.mem_of_mem h)

[Patrick Massot]

I am not surprised. This is a pretty specific statement. Where do you need this?

[Anatole Dedecker]

What I really want is a simple way to get a basis of 𝓝 x which is both countable and made of open sets (with a FirstCountableTopology hypothesis of course). Maybe I've missed it, but I figured the simplest way was to take a countable basis and replace each set by its interior. The reason I want open neighborhoods is I want them measurable.

[Anatole Dedecker]

In the same vein we have docs#Filter.HasBasis.nhds_closure

[Anatole Dedecker]

Of course the "real" lemma is a docs#Filter.lift' statement, but I couldn't find it either...

[Yury G. Kudryashov]

Sorry, I forgot to PR it with Filter.HasBasis.lift'_closure etc

[Yury G. Kudryashov]

I can open a PR that mirrors the closure API later today.

[Anatole Dedecker]

Thanks! And no worries of course!

[Yury G. Kudryashov]

#10175

[Yury G. Kudryashov]

As for your #xy problem, we have docs#Filter.HasBasis.exists_antitone_subbasis and docs#Filter.IsMeasurablyGenerated

[Yury G. Kudryashov]

The latter could use a rewrite using Filter.HasBasis. Also, we have this "has subbasis in sets with property" here and there; should we add it as a typeclass?

[Anatole Dedecker]

Thanks a lot Yury! I thought about something like IsMeasurablyGenerated but for some reason I didn't even check wether it existed :face_palm: Regardless of the rewriting, do we have a lemma expressing it in terms of bases?