Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-22 20:00 5080d64d

View on Github →

feat(topology): add a few lemmas (#11607)

  • add homeomorph.preimage_interior, homeomorph.image_interior, reorder lemmas;
  • add is_open.smul₀ and interior_smul₀.

Estimated changes

added theorem interior_smul₀
added theorem is_open.smul₀