Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-14 03:22 69d71341

View on Github โ†’

feat(topology/basic): f =แถ [๐“ a] 0 iff a โˆ‰ closure (support f) (#6665) Also add equiv.image_symm_image and function.compl_support.

Estimated changes

added theorem equiv.image_symm_image
modified theorem equiv.symm_image_image
added theorem function.compl_support