Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-23 09:40 e7c75527

View on Github →

feat(analysis/topology/continuity): compactness and embeddings

Estimated changes

Modified analysis/topology/continuity.lean

added theorem compact_iff_compact_image_of_embedding

added theorem compact_iff_compact_in_subtype

added theorem compact_iff_compact_univ

added theorem embedding.continuous

added theorem quotient_map.continuous