Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-01 10:20 206a7a11

View on Github →

feat(*): add various small lemmas

Estimated changes

Modified src/analysis/normed_space/basic.lean

added theorem norm_norm

added theorem normed_space.tendsto_nhds_zero

added theorem tendsto_smul_const

Modified src/order/filter/basic.lean

added theorem filter.le_comap_top

added theorem filter.tendsto.congr

Modified src/topology/basic.lean

deleted theorem tendsto_at_within_iff_subtype

added theorem tendsto_nhds_within_iff_subtype

added theorem tendsto_nhds_within_mono_left

added theorem tendsto_nhds_within_mono_right

added theorem tendsto_nhds_within_of_tendsto_nhds

Modified src/topology/continuity.lean

added theorem nhds_within_le_comap