Theorem RestrictGenTopology.of_isClosed

Modification history

2024-11-11 19:06

Mathlib/Topology/RestrictGen.lean

chore(Topology): Namespace `Inducing`, `Embedding`... (#15993) …

Deleted RestrictGenTopology.of_isClosed View on Github →

2024-06-29 22:58

Mathlib/Topology/RestrictGenTopology.lean

feat: define `RestrictGenTopology` (#13452)

Added RestrictGenTopology.of_isClosed View on Github →