mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(topology/metric_space/emetric_space): `nhds_within` lemmas

Open YaelDillies opened this issue 3 years ago • 0 comments

A few lemmas about emetric spaces and nhds_within.

Note, I don't need those lemmas. I just found myself writing them before figuring out another approach.

Open in Gitpod

YaelDillies avatar Oct 13 '22 16:10 YaelDillies