# Zulip Chat Archive

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

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

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

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

(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