Commit 2023-10-25 20:01 c60a7805

View on Github →

feat(NhdsSet): lemmas from the Mandelbrot set connectedness project (#7914) Add eventually_nhdsSet_iff_exists, eventually_nhdsSet_iff_forall, and IsOpen.mem_nhdsSet_self.

Estimated changes

Modified Mathlib/Topology/NhdsSet.lean

added theorem IsOpen.mem_nhdsSet_self

added theorem eventually_nhdsSet_iff_exists

added theorem eventually_nhdsSet_iff_forall