### Topic Contiguity ### Question Fill in the sorry in line 147 in https://github.com/stat-lib/statlib/pull/10, and the proof can be found below: <img width="923" height="259" alt="Image" src="https://github.com/user-attachments/assets/b98ae62b-9ba2-4bd5-a5bd-a4e548365c71" /> I proved in #10 `Filter.tendsto_of_forall_filter_le_exists_tendsto`, which I believe can be useful for this theorem. ### Links or references _No response_
Topic
Contiguity
Question
Fill in the sorry in line 147 in #10, and the proof can be found below:
I proved in #10
Filter.tendsto_of_forall_filter_le_exists_tendsto, which I believe can be useful for this theorem.Links or references
No response