Trying to understand nhdsSet

Stream: general

[Trevor Murphy]

I'm learning about filters through some basic exercises on normed topological vector spaces over the reals. One question that arose for me was this: can I show the following

example {X : Type*} [SeminormedAddCommGroup X] [NormedSpace ℝ X]
    {U V : Set X} : 𝓝ˢ (U + V) = 𝓝ˢ U + 𝓝ˢ V := sorry

If not, are there hypotheses I can add to U and/or V that make it true in a nontrivial way? Intuitively I'm pretty sure that the "≤" direction is true in general, though I'm still struggling to formalize a proof. But I'm really struggling to think about the "≥" direction. I can't think of a counterexample, but I also get easily confused when trying to unravel the definitions.

Is somebody able to point me in a useful direction?

[Kevin Buzzard]

Can you edit your post to make it a #mwe ? So far I tried adding import Mathlib and open scoped Topology but your code still doesn't compile so I don't even know what the question says.

[Kevin Buzzard]

Oh finally got it: is this your question?

import Mathlib

open scoped Topology Pointwise

example {X : Type*} [SeminormedAddCommGroup X] [NormedSpace ℝ X]
    {U V : Set X} : 𝓝ˢ (U + V) = 𝓝ˢ U + 𝓝ˢ V := sorry

Can you give a mathematics proof of what you're claiming here? i.e. are you asking a mathematics question or a Lean question?

[Trevor Murphy]

Ah sorry for the confusion. There's a math question and a lean question. Here's the lean part first:

The claim 𝓝ˢ (U + V) ≤ 𝓝ˢ U + 𝓝ˢ V holds generally. Let W be any set in 𝓝ˢ U + 𝓝ˢ V, and let U' and V' be open sets with U ⊆ U', V ⊆ V', and U' + V' ⊆ W. Then U' + V' is an open set with U + V ⊆ U' + V' ⊆ W, so W is in 𝓝ˢ (U + V). I'm stuck translating this into lean because I don't understand the nhdsSet API well enough to pull out the U' and V' that satisfy those conditions.

[Trevor Murphy]

Then there's a math question about the reverse inequality. It feels like there should be a counterexample, but I'm just not coming up with it. I was hoping maybe the API and general lean code around nhdsSet could point me in a useful direction but I couldn't figure it out.

Alternatively, it feels like if I assume U and V are nice enough (maybe connected?) then it should be possible to prove the reverse inequality. Again I was hoping to glean some ideas from the conditions and properties of nhdsSet, but I couldn't figure it out.

[Kevin Buzzard]

import Mathlib

open scoped Topology Pointwise

example {X : Type*} [SeminormedAddCommGroup X] [NormedSpace ℝ X]
    {U V : Set X} : 𝓝ˢ (U + V) ≤ 𝓝ˢ U + 𝓝ˢ V := by
  -- let W be any set in N(U)+N(V)
  intro W hW
  -- by definition
  -- let A, B be sets with U ⊆ interior(A), V ⊆ interior(B), and A + B ⊆ W
  obtain ⟨A, hA, B, hB, h⟩ := hW
  -- let U' and V' be opens with U ⊆ U' ⊆ A and V ⊆ V' ⊆ B
  rw [mem_nhdsSet_iff_exists] at hA hB
  obtain ⟨U', hU', hUU', HU'A⟩ := hA
  obtain ⟨V', hV', hVV', hV'B⟩ := hB
  -- we want to find some open W' with U + V ⊆ W' ⊆ W
  rw [mem_nhdsSet_iff_exists]
  -- We claim U' + V' works
  use U' + V'
  -- is an open set with U + V ⊆ U' + V' ⊆ W
  -- so we now need to check it's open, it contains U+V and it's contained in W
  refine ⟨?_, ?_, ?_⟩
  · -- U' + V' is open because it's a union of open sets (translate of V')
    exact IsOpen.add_left hV'
  · -- the inclusion U + V ⊆ U' + V' is clear by monotonicity results
    mono
  · -- and the inclusion U' + V' ⊆ W is also clear
    apply subset_trans (show U' + V' ⊆ A + B by mono) h

is the inclusion which we have the proof of.

[Mirek Olšák]

If I understand the definitions well, this should be a counterexample to the math question:

• $X = \R^2$
• $U = \{(n,0) \mid n \in \Z\}$
• $V = \{(0,n) \mid n \in \Z\}$
• A neighborhood of $U+V$ where we take a ball of radius $\min(1, e^{-x-y})$ around each integer point.

[Trevor Murphy]

Okay! Thanks so much! I'll go work through these

[Mirek Olšák]

I don't think connectedness helps much, then I could connect the disconnected points through another dimension. Compactness of $U+V$ should help, then for a given neighborhood of $U+V$, we can find an $\epsilon$-neighborhood inside.

[Trevor Murphy]

Ah now I see how that example works. Interesting, thanks for explaining. I'll have a lot to think about on the plane home

[Kevin Buzzard]

How about $X=\R^2$, $U=(-1,1)\times\{0\}$, $V=\{0\}\times(-1,1)$ and the neighbourhood is simply $U+V=(-1,1)\times(-1,1)$?