add paracompact properties and arens space props

properties/P000145.md

@@ -0,0 +1,12 @@
+---
+uid: P000145
+slug: strongly-paracompact
+name: Strongly paracompact
+refs:
+  - mr: MR1039321
+    name: General Topology (Engelking, 1989)
+---
+
+Every open cover has a star-finite open refinement.
+
+Defined on p. 326 of {{mr:MR1039321}} together with the condition that the space is {P3}.  Here we do not assume any separation axiom as part of the definition.

properties/P000146.md

@@ -0,0 +1,14 @@
+---
+uid: P000146
+slug: ultraparacompact
+name: Ultraparacompact
+refs:
+  - doi: 10.48550/arXiv.1306.6086
+    name: Ultraparacompactness and Ultranormality (J. Van Name)
+  - mr: MR261565
+    name: Extending continuous functions on zero-dimensional spaces (R. Ellis)
+---
+
+Every open cover of the space has an open (hence clopen) refinement partitioning the space. (We do not assume {P3}.)
+
+Equivalently, every open cover of the space is refined by a locally finite clopen cover.  The equivalence between the two definitions is shown in Lemma 1.3 and Corollary 1.4 of {{mr:MR261565}} (<https://eudml.org/doc/161976>).

spaces/S000156/properties/P000001.md

@@ -0,0 +1,10 @@
+---
+space: S000156
+property: P000001
+value: true
+refs:
+- mathse: 4673615
+  name: What separation properties are satisfied by the Arens space?
+---
+
+Points are topologically distinct.

spaces/S000156/properties/P000050.md

@@ -0,0 +1,10 @@
+---
+space: S000156
+property: P000050
+value: true
+refs:
+- mathse: 4673615
+  name: What separation properties are satisfied by the Arens space?
+---
+
+Basic open sets in a convergent sequence are clopen; this passes to {S156}.

theorems/T000342.md

@@ -0,0 +1,12 @@
+---
+uid: T000342
+if:
+  P000146: true
+then:
+  P000145: true
+refs:
+  - mathse: 4673639
+    name: Answer to What separation properties are satisfied by the Arens space?
+---
+
+Any partition is star-finite.

theorems/T000343.md

@@ -0,0 +1,14 @@
+---
+uid: T000343
+if:
+  P000145: true
+then:
+  P000030: true
+refs:
+  - mr: MR1039321
+    name: General Topology (Engelking, 1989)
+---
+
+Any star-finite collection of open sets is locally finite.
+
+Stated on p. 326 of {{mr:MR1039321}}.

theorems/T000344.md

@@ -0,0 +1,14 @@
+---
+uid: T000344
+if:
+  and:
+    - P000018: true
+    - P000050: true
+then:
+  P000146: true
+refs:
+  - doi: 10.48550/arXiv.1306.6086
+    name: Ultraparacompactness and Ultranormality (J. Van Name)
+---
+
+See Proposition 4 of {{doi:10.48550/arXiv.1306.6086}}.