Anatole Dedecker comments

Results 25 comments of


                                            Anatole Dedecker

feat: "outer product" of functions that tend to zero on the cocompact filter

Very nice work, thanks a lot! I think it would be nice to split up some useful lemmas from the main proof, e.g a version of [Filter.Tendsto.zero_mul_isBoundedUnder_le](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Normed/Field/Basic.html#Filter.Tendsto.zero_mul_isBoundedUnder_le) where the "IsBoundedUnder"...

feat: "outer product" of functions that tend to zero on the cocompact filter

You don't have to apologize at all! In fact I should probably be the one apologizing for causing troubles by giving unclear instructions. What I had in mind is the...

feat: "outer product" of functions that tend to zero on the cocompact filter

I just pushed what I had in mind!

chore: reorganize and rename the Embedding --> Homeomorph constructions

Sorry, I was having a pretty rough time at this period last year. I'll update this.

chore: reorganize and rename the Embedding --> Homeomorph constructions

See #24113.