frequently_in_nhds_map

Stream: Is there code for X?

[Scott Morrison]

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]

Or is there some more idiomatic way to state it?

[Kevin Buzzard]

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]

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

[Scott Morrison]

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]

I don't know what nhds p means

[Kevin Buzzard]

docs#filter.nhds

[Kevin Buzzard]

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

[Kevin Buzzard]

I don't understand h

[Scott Morrison]

Notice it is ∃ᶠ, not ∃.

[Scott Morrison]

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

[Kevin Buzzard]

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

[Heather Macbeth]

@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]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

(deleted)

[Scott Morrison]

Or is it just too obvious? :-)

[Heather Macbeth]

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]

Then your lemma could be proved as

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

[Heather Macbeth]

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]

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]

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

[Heather Macbeth]

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

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