Commit 2023-02-12 21:31 15185f35

View on Github →

feat: Port Topology.ContinuousFunction.T0Sierpinski (#2240) Comments update and reflow only.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/ContinuousFunction/T0Sierpinski.lean

added theorem TopologicalSpace.eq_induced_by_maps_to_sierpinski

added def TopologicalSpace.productOfMemOpens

added theorem TopologicalSpace.productOfMemOpens_embedding

added theorem TopologicalSpace.productOfMemOpens_inducing

added theorem TopologicalSpace.productOfMemOpens_injective