Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-16 20:16 8685bf2d

View on Github →

refactor(topology/continuity): remove inhabited from dense extend

Estimated changes

Modified analysis/topology/continuity.lean

deleted theorem dense_embedding.continuous_ext

added theorem dense_embedding.continuous_extend

deleted def dense_embedding.ext

deleted theorem dense_embedding.ext_e_eq

deleted theorem dense_embedding.ext_eq

added def dense_embedding.extend

added theorem dense_embedding.extend_e_eq

added theorem dense_embedding.extend_eq

deleted theorem dense_embedding.tendsto_ext

added theorem dense_embedding.tendsto_extend

Modified analysis/topology/uniform_space.lean