Theorem TopologicalSpace.eq_induced_by_maps_to_sierpinski

Modification history

2023-08-10 19:52
Mathlib/Topology/ContinuousFunction/T0Sierpinski.lean
chore: banish `Type _` and `Sort _` (#6499) …
Modified TopologicalSpace.eq_induced_by_maps_to_sierpinskiView on Github →
2023-02-12 21:31
Mathlib/Topology/ContinuousFunction/T0Sierpinski.lean
feat: Port Topology.ContinuousFunction.T0Sierpinski (#2240) …
Added TopologicalSpace.eq_induced_by_maps_to_sierpinskiView on Github →