Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-20 15:24 d47a6e33

View on Github →

feat(topology): clopens form a topology basis for profinite sets (#7671) from LTE

Estimated changes

Modified src/topology/basic.lean

added theorem exists_open_set_nhds'

added theorem exists_open_set_nhds

Modified src/topology/separation.lean

added theorem exists_subset_nhd_of_compact

added theorem is_topological_basis_clopen

added theorem nhds_basis_clopen

Modified src/topology/subset_properties.lean

added theorem exists_subset_nhd_of_compact'

added theorem exists_subset_nhd_of_compact_space

added theorem is_clopen_Union

added theorem is_clopen_bUnion