leanprover-community / leanprover-community/mathlib4
Investigate a potential "filter-indexed" version of Filter.HasBasis
Open
Nobody has claimed this yet.
- Dominant language
- Lean
- Stars
- 4.1k
- Forks
- 1.7k
- PR merge metrics
- No merged PRs in 30d
Description
This is motivated by generalizing statements like
theorem Metric.tendsto_nhds' {f : Filter β} {u : β → α} {a : α} :
Tendsto u f (𝓝 a) ↔ ∀ᶠ ε in 𝓝[>] 0, ∀ᶠ x in f, dist (u x) a < ε`
which correspond to the fact the basis of 𝓝 a made of balls of radius ε would be "naturally indexed by the filter 𝓝[>] 0", whatever that means.
Originally discussed on Zulip
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start with Filter.HasBasis and the Metric.tendsto_nhds' example in the issue, then read the linked Zulip discussion for the intended meaning of a basis indexed by a filter. A useful outcome would define whether this generalization is appropriate and specify an agreed API that supports the motivating theorem.
Written by the indexing model from the issue text.
Assessment
- Domain
- tooling
- Issue type
- Feature
- Difficulty
- 5/5
- Estimated time
- Over a week
- Activity status
- Stale
- Clarity
- Needs clarification
- Newbie friendliness
- 25/100