Basic ∀ᶠ and 𝓝 usage

Stream: Is there code for X?

[Thomas Murrills]

Given ∀ᶠ (x : ℝ) in 𝓝 a, P x, is there a simple way to get P a without going through eventually/ball-lemmas? I feel there should be a simple way to do it, but I couldn't find it with loogle...

[Yaël Dillies]

docs#Filter.Eventually.exists ?

[Yaël Dillies]

Oh sorry I see it's the same a!

[Yaël Dillies]

docs#Filter.Eventually.self_of_nhds

[Thomas Murrills]

Ah, great, thanks! :D

[Thomas Murrills]

(Oh, I just realized why I couldn't get it with loogle! I wrote ∀ᶠ (y : _) in nhds _, _ -> _ instead of (∀ᶠ (y : _) in nhds _, _) -> _ :P )

[Thomas Murrills]

Hmm, given f : A → B, ∀ᶠ (b : B) in 𝓝 (f a₀), P b, and ContinuousAt f a₀, can we get ∀ᶠ (a : A) in 𝓝 a₀, P (f a) via the preimage? Or is that not true in general/with these primitives? (I checked my loogle query's parentheses this time!)

[Thomas Murrills]

Ah, given hcf : ContinuousAt f a₀ and h : ∀ᶠ (b : B) in 𝓝 (f a₀), P b, you can literally just write hcf h. Never would have guessed, thanks hint! :)

[Thomas Murrills]

Ah, but you do have to coerce the type afterwards. (Maybe it would be worth having a definition for type purposes (and for apply? etc. to use).)

[Patrick Massot]

We do have docs#Filter.Tendsto.eventually. Isn't it what you want?

[Thomas Murrills]

Oh, looks like it! I suppose my searches were too restrictive—I was including nhds after in.