ハウスドルフトポロジカルスペース（空間）に対して、もしも、ローカルにコンパクトハウスドルフトポロジカルスペース（空間）でスペース（空間）がそのローカルにクローズド（閉）サブスペース（部分空間）であるものがある場合、スペース（空間）はローカルにコンパクトであることの記述/証明
話題
About: トポロジカルスペース（空間）
この記事の目次
開始コンテキスト
- 読者は、ハウスドルフトポロジカルスペース（空間）の定義を知っている。
- 読者は、ローカルにコンパクトなトポロジカルスペース（空間）の定義を知っている。
- 読者は、ローカルにクローズド（閉）トポロジカルサブスペース（部分空間）の定義を知っている。
- 読者は、トポロジカルサブスペース（部分空間）の定義を知っている。
- 読者は、任意のトポロジカルサブスペース（部分空間）はローカルにクローズド（閉）である、もしも、それがベーススペース（空間）のあるクローズドサブセット（部分集合）とあるオープンサブセット（開部分集合）のインターセクション（共通集合）である場合、そしてその場合に限って、という命題を認めている。
- 読者は、任意のローカルにコンパクトなトポロジカルスペース（空間）の任意のクローズド（閉）サブスペース（部分空間）はローカルにコンパクトであるという命題を認めている。
- 読者は、任意のハウスドルフトポロジカルスペース（空間）の任意のサブスペース（部分空間）はハウスドルフであるという命題を認めている。
- 読者は、任意のローカルにコンパクトなハウスドルフトポロジカルスペース（空間）の任意のオープン（開）サブスペース（部分空間）はローカルにコンパクトであるという命題を認めている。
- 読者は、トポロジカルサブスペース（部分空間）たちの任意のネストにおいて、任意のサブスペース（部分空間）上の任意のサブセット（部分集合）のオープン（開）性は、当該サブスペース（部分空間）がサブスペース（部分空間）とみなされる元のスーパースペース（空間）に依存しないという命題を認めている。
ターゲットコンテキスト
- 読者は、任意のハウスドルフトポロジカルスペース（空間）に対して、もしも、あるローカルにコンパクトハウスドルフトポロジカルスペース（空間）で当該スペース（空間）がそのローカルにクローズド（閉）サブスペース（部分空間）であるものがある場合、当該スペース（空間）はローカルにコンパクトであるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(T\): \(\in \{\text{ 全てのハウスドルフトポロジカルスペース（空間）たち }\}\)
//
ステートメント（言明）たち:
\(\exists T' \in \{\text{ 全てのローカルにコンパクトハウスドルフトポロジカルスペース（空間）たち }\} (T \in \{T' \text{ の全てのローカルにクローズド（閉）サブスペース（部分空間）たち }\})\)
\(\implies\)
\(T \in \{\text{ 全てのローカルにコンパクトトポロジカルスペース（空間）たち }\}\)
//
2: 証明
全体戦略: ステップ1: \(T = C' \cap U'\)、あるクローズド（閉）\(C' \subseteq T'\)およびあるオープン（開）\(U' \subseteq T'\)に対して、であることを見る; ステップ2: \(C'\)はローカルにコンパクトであり\(T\)は\(C'\)のあるローカルにコンパクトサブスペース（部分空間）であることを見る。
ステップ1:
以下を満たすあるクローズド（閉）\(C' \subseteq T'\)およびあるオープン（開）\(U' \subseteq T'\)、つまり、\(T = C' \cap U'\)、がある、任意のトポロジカルサブスペース（部分空間）はローカルにクローズド（閉）である、もしも、それがベーススペース（空間）のあるクローズドサブセット（部分集合）とあるオープンサブセット（開部分集合）のインターセクション（共通集合）である場合、そしてその場合に限って、という命題によって。
ステップ2:
\(C' \subseteq T'\)はあるローカルにコンパクトハウスドルフトポロジカルサブスペース（部分空間）である、任意のローカルにコンパクトなトポロジカルスペース（空間）の任意のクローズド（閉）サブスペース（部分空間）はローカルにコンパクトであるという命題および任意のハウスドルフトポロジカルスペース（空間）の任意のサブスペース（部分空間）はハウスドルフであるという命題によって。
\(T = C' \cap U' \subseteq C'\)、\(C'\)のトポロジカルサブスペース（部分空間）として、は、あるオープンサブスペース（開部分空間）である、トポロジカルサブスペース（部分空間）の定義によって、そして、\(C'\)のあるローカルにコンパクトトポロジカルサブスペース（部分空間）である、任意のローカルにコンパクトなハウスドルフトポロジカルスペース（空間）の任意のオープン（開）サブスペース（部分空間）はローカルにコンパクトであるという命題によって。
しかし、\(T\)、\(C'\)のトポロジカルサブスペース（部分空間）として、は、\(T\)、\(T'\)のトポロジカルサブスペース（部分空間）として、である、トポロジカルサブスペース（部分空間）たちの任意のネストにおいて、任意のサブスペース（部分空間）上の任意のサブセット（部分集合）のオープン（開）性は、当該サブスペース（部分空間）がサブスペース（部分空間）とみなされる元のスーパースペース（空間）に依存しないという命題によって。
私たちが話題にしている\(T\)は\(T'\)のトポロジカルサブスペース（部分空間）であるから、\(T\)はローカルにコンパクトである。
