Theorem TopologicalSpace.Opens.openEmbedding'

Modification history

2024-10-18 21:29

Mathlib/Topology/Sets/Opens.lean

chore: Rename `OpenEmbedding` to `IsOpenEmbedding` (#17898) …

Deleted TopologicalSpace.Opens.openEmbedding'View on Github →

2023-12-07 08:20

Mathlib/Topology/Sets/Opens.lean

feat: a function with vanishing integral against smooth functions supported in U is ae zero in U (#8805) …

Added TopologicalSpace.Opens.openEmbedding'View on Github →