Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-08 09:28 8e4aafab

View on Github →

feat(analysis/metric): convergence wrt nhds_within

Estimated changes

Modified analysis/metric_space.lean

added theorem metric.mem_nhds_within

added theorem metric.ptendsto_nhds_within

added theorem metric.rtendsto'_nhds_within

added theorem metric.rtendsto_nhds_within

added theorem metric.tendsto_nhds_within