Add Hereditarily Lindelöf + KC ⇒ Strongly KC (#1187)

pi-base · Jan 9, 2025 · ea7313c · ea7313c
1 parent cbc3cb6
commit ea7313c
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 15 deletions.
diff --git a/spaces/S000017/properties/P000103.md b/spaces/S000017/properties/P000103.md
diff --git a/theorems/T000690.md b/theorems/T000690.md
@@ -0,0 +1,13 @@
+---
+uid: T000690
+if:
+  and:
+  - P000100: true
+  - P000131: true
+then:
+  P000103: true
+---
+
+Let $A \subseteq X$ be a {P19} subset. It must be {P18} because $X$ is {P131}.
+
+Since {P18} {P19} spaces are {P16}, we know $A$ is {P16}. Thus $A$ is closed since $X$ is {P100}.