Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-09 18:57 2b9aca75

View on Github →

feat(topology): a few more results about compact sets (#11905)

Also a few lemmas about sets and mul_support.

Estimated changes

Modified src/algebra/support.lean

added theorem function.disjoint_mul_support_iff

added theorem function.mul_support_disjoint_iff

Modified src/data/set/basic.lean

added theorem set.compl_ne_univ

added theorem set.not_mem_compl_iff

Modified src/topology/algebra/group.lean

added theorem is_compact.inv

Modified src/topology/algebra/monoid.lean

added theorem is_compact.mul

Modified src/topology/separation.lean

added theorem exists_compact_superset_iff