PR #13500: uniform_limit_of_holo_is_holo

Stream: triage

[Random Issue Bot]

Today I chose PR 13500 for discussion!

uniform_limit_of_holo_is_holo
Created by @Chris Birkbeck (@CBirkbeck) on 2022-04-18
Labels: WIP

Is this PR still relevant? Any recent updates? Anyone making progress?

[Chris Birkbeck]

No its been replaced by #17074 (at least the final result, other bits may still appear in mathlib, but separately)

[Riccardo Brasca]

Can we close it?

[Chris Birkbeck]

yep!