@[reducible, inline]

abbrev PiBase.ArtinianSpace (X : Type u_1) [TopologicalSpace X] : Prop

Equations

• PiBase.ArtinianSpace X = WellFoundedGT (TopologicalSpace.Closeds X)