Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-24 20:17 e4c09d4e

View on Github →

feat(analysis/topology/topological_space): a finite union of compact sets is compact (#117)

Estimated changes

Modified analysis/topology/topological_space.lean

added theorem compact_bUnion_of_compact

added theorem compact_of_finite