Theorem Continuous.tendsto_nhdsSet_nhds

Modification history

2024-01-12 06:00

Mathlib/Topology/NhdsSet.lean

chore(Topology/NhdsSet): rename type variables (#9673) …

Modified Continuous.tendsto_nhdsSet_nhds View on Github →

2023-10-31 02:45

Mathlib/Topology/NhdsSet.lean

feat(Topology/CompletelyRegular): Add definition `CompletelyRegularSpace` (#7926) …

Added Continuous.tendsto_nhdsSet_nhds View on Github →