## Stream: Is there code for X?

### Topic: frequently_in_nhds_map

#### 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!

#### Scott Morrison (Mar 19 2021 at 07:03):

Or is there some more idiomatic way to state it?

#### 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

#### Scott Morrison (Mar 19 2021 at 07:15):

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

#### 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? :-)

#### Kevin Buzzard (Mar 19 2021 at 07:17):

I don't know what nhds p means

docs#filter.nhds

#### Kevin Buzzard (Mar 19 2021 at 07:23):

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

#### Kevin Buzzard (Mar 19 2021 at 07:24):

I don't understand h

#### Scott Morrison (Mar 19 2021 at 07:43):

Notice it is ∃ᶠ, not ∃.

#### Scott Morrison (Mar 19 2021 at 07:43):

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

#### 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

#### 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))


#### Scott Morrison (Mar 19 2021 at 22:45):

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

#### Scott Morrison (Mar 19 2021 at 22:45):

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

#### Scott Morrison (Mar 19 2021 at 22:45):

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

(deleted)

#### Scott Morrison (Mar 19 2021 at 22:47):

Or is it just too obvious? :-)

#### 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.

#### Heather Macbeth (Mar 19 2021 at 22:48):

Then your lemma could be proved as

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


#### 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.

#### 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))


#### Scott Morrison (Mar 20 2021 at 03:20):

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

#### 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