Def TopologicalSpace.productOfMemOpens

Modification history

2023-02-12 21:31

Mathlib/Topology/ContinuousFunction/T0Sierpinski.lean

feat: Port Topology.ContinuousFunction.T0Sierpinski (#2240) …

Added TopologicalSpace.productOfMemOpens View on Github →