Commit 2024-01-30 02:26 15e555e7

View on Github →

feat: characterize "eventually" in a subtype (#7568)

Estimated changes

Modified Mathlib/Topology/ContinuousOn.lean

added theorem eventually_nhds_subtype_if

added theorem frequently_nhds_subtype_iff