Zulip Chat Archive

Stream: Is there code for X?

Topic: frequently_in_nhds_map


view this post on Zulip Scott Morrison (Mar 19 2021 at 06:54):

Help with filters again, please! :-)

import topology.basic

example {X Y : Type*} [topological_space X] [topological_space Y]
  (P : X  Prop) (Q : Y  Prop) (f : X  Y) (c : continuous f) (w :  x, P x  Q (f x))
  (p : X) (h : ∃ᶠ x in nhds p, P x) : ∃ᶠ y in nhds (f p), Q y :=
sorry

Is this available somewhere? If not, advice on slick proof and/or name appreciated!

view this post on Zulip Scott Morrison (Mar 19 2021 at 07:03):

Or is there some more idiomatic way to state it?

view this post on Zulip Kevin Buzzard (Mar 19 2021 at 07:14):

Your w is just tendsto f (\P P) (\P Q) but I don't know if this helps. Here \P is principal filter

view this post on Zulip Scott Morrison (Mar 19 2021 at 07:15):

(Took me a moment to work out the \Ps :-)

view this post on Zulip Scott Morrison (Mar 19 2021 at 07:16):

Oh dear, so this is going to drop out of some incredibly general thing where we replace P and Q by filters too? :-)

view this post on Zulip Kevin Buzzard (Mar 19 2021 at 07:17):

I don't know what nhds p means

view this post on Zulip Kevin Buzzard (Mar 19 2021 at 07:18):

docs#filter.nhds

view this post on Zulip Kevin Buzzard (Mar 19 2021 at 07:23):

I'm confused about how an element can be in a neighborhood filter

view this post on Zulip Kevin Buzzard (Mar 19 2021 at 07:24):

I don't understand h

view this post on Zulip Scott Morrison (Mar 19 2021 at 07:43):

Notice it is ∃ᶠ, not .

view this post on Zulip Scott Morrison (Mar 19 2021 at 07:43):

so it is saying there are x arbitrarily close to p such that P X.

view this post on Zulip Kevin Buzzard (Mar 19 2021 at 07:53):

Oh I can't see some symbols on my phone. I wish I knew how to fix this

view this post on Zulip Heather Macbeth (Mar 19 2021 at 17:33):

@Scott Morrison

import topology.basic

example {X Y : Type*} [topological_space X] [topological_space Y]
  (P : X  Prop) (Q : Y  Prop) (f : X  Y) (c : continuous f) (w :  x, P x  Q (f x))
  (p : X) (h : ∃ᶠ x in nhds p, P x) : ∃ᶠ y in nhds (f p), Q y :=
c.continuous_at.tendsto.frequently (h.mp (filter.eventually_of_forall w))

view this post on Zulip Scott Morrison (Mar 19 2021 at 22:45):

Fantastic. My proof broke through both the filter API and the set API. :-)

view this post on Zulip Scott Morrison (Mar 19 2021 at 22:45):

Could I add this, calling it e.g. frequently_in_nhds_map?

view this post on Zulip Scott Morrison (Mar 19 2021 at 22:45):

(I'll probably reduce the hypothesis to just use continuous_at directly.)

view this post on Zulip Scott Morrison (Mar 19 2021 at 22:45):

(deleted)

view this post on Zulip Scott Morrison (Mar 19 2021 at 22:47):

Or is it just too obvious? :-)

view this post on Zulip Heather Macbeth (Mar 19 2021 at 22:47):

I'd be inclined to add versions of docs#filter.eventually.mp and docs#filter.frequently.mp which take a hypothesis with , rather than ∀ᶠ -- there are several other places in the library where we have both versions.

view this post on Zulip Heather Macbeth (Mar 19 2021 at 22:48):

Then your lemma could be proved as

c.continuous_at.tendsto.frequently (h.mp' w)

view this post on Zulip Heather Macbeth (Mar 19 2021 at 22:51):

What do you think? If you'd like to add another intermediate fact, I'd suggest splitting it at the tendsto point rather than the continuous_at point.

view this post on Zulip Heather Macbeth (Mar 19 2021 at 22:52):

i.e. something like

import order.filter.basic

lemma filter.tendsto.frequently_map {X Y : Type*} (l₁ : filter X) (l₂ : filter Y)
  (P : X  Prop) (Q : Y  Prop) (f : X  Y) (c : filter.tendsto f l₁ l₂) (w :  x, P x  Q (f x))
  (h : ∃ᶠ x in l₁, P x) : ∃ᶠ y in l₂, Q y :=
c.frequently (h.mp (filter.eventually_of_forall w))

view this post on Zulip Scott Morrison (Mar 20 2021 at 03:20):

It seems eventually.mp' already exists as eventually.mono.

view this post on Zulip Heather Macbeth (Mar 20 2021 at 03:46):

Oh, in fact there's docs#filter.frequently.mono too!

c.continuous_at.tendsto.frequently (h.mono w)

Last updated: May 19 2021 at 02:10 UTC