ContinuousAt.eventually_mem'

Stream: mathlib4

[Geoffrey Irving]

Is this lemma reasonable to add?

theorem ContinuousAt.eventually_mem' {A B : Type} [TopologicalSpace A] [TopologicalSpace B]
    {f : A → B} {x : A} (fc : ContinuousAt f x) {s : Set B} (m : s ∈ 𝓝 (f x)) :
    ∀ᶠ y in 𝓝 x, f y ∈ s :=
  fc m

It almost exists now, as Filter.Tendsto.eventually_mem. However, that lemma has no connection between the xs occuring in the two locations. I turn out to use apply ContinuousAt.eventually_mem' a lot, and a lot of those applies no longer infer if replaced by Filter.Tendsto.eventually_mem.

[Geoffrey Irving]

Hmm, actually I don't think I understand why it doesn't infer. I should produce a MWE, but unfortunately I have to head off now.

[Patrick Massot]

Why the prime? Is there an unprimed version?

[Geoffrey Irving]

The unprimed version is Filter.Tendsto.eventually_mem, but maybe that’s fine.

[Geoffrey Irving]

That is, the goal was not to shadow when using dot notation, but I suppose the new one should match when the old one did.

[Geoffrey Irving]

(Since ContinuousAt is a Filter.Tendsto)

[Patrick Massot]

I don’t think there would be any shadowing.

[Geoffrey Irving]

There’s definitely shadowing: currently if you have a c : ContinuousAt and you do c.eventually_mem you get Filter.Tendsto.eventually_mem.

[Geoffrey Irving]

So my guess on reflection is that adding this is a clean (small) win, as all/nearly all shadowing examples will still work, and the new one is better for inference. If that seems reasonable I can make a PR to check the “still work” part.

[Anatole Dedecker]

Yes, I think your proposed new lemma is precisely what you already get by doing c.eventually_mem but with better inference properties, so I think it is a good idea.

[Geoffrey Irving]

https://github.com/leanprover-community/mathlib4/pull/10838

[Geoffrey Irving]

Indeed, all of Mathlib built without complaint.

[Geoffrey Irving]

(And I can reconfirm that this one is way better for use with apply.)