Mathlib Map

Structures · Topology

PerfectlyNormalSpace

A topological space X is a perfectly normal space provided it is normal and closed sets are Gδ.

Defined in
Mathlib.Topology.Separation.GDelta
Shape
One type argument · adds closed_gdelta

Extends1

Extended by1

Concrete types that are instances1

  • Set.Elem

How is a type an instance?

Loading the hierarchy index…

Assumed by8

Ancestors1