Theorem eventually_nhds_subtype_if

Modification history

2024-01-31 10:21
Mathlib/Topology/ContinuousOn.lean
feat: fix typo (eventually_nhds_subtype_if -> eventually_nhds_subtype_iff) (#10124) …
Deleted eventually_nhds_subtype_ifView on Github →
2024-01-30 02:26
Mathlib/Topology/ContinuousOn.lean
feat: characterize "eventually" in a subtype (#7568)
Added eventually_nhds_subtype_ifView on Github →