結局、数学の機能語とは、
∀x (for all x)
∃x (there exists x such that)
¬ (not)
∧ (and) ※ 簡潔さのため "," を ∧ の意味で使う
∨ (or)
⇨ (implies)
⇔ (iff: if and only if)
だけなのである。このうち、implies ⇨ だけが、理解が徹底していないと適切に使えないかもしれないので、念のため説明したのである。
※ 写像の→ と混同する恐れがあるときは、今後 implies は ⇨ で書く。
後は
¬∃ x(P(x)) ≡ ∀x(¬P(x))
¬∀ x(P(x)) ≡ ∃x(¬P(x))
を含めたドモルガンの法則ぐらいで十分であろう。なんという簡潔さだろう! 証明すべき命題もほとんどが全称命題か存在命題のどちらかである。
さて、寄り道はやめて距離空間に戻るが、これからは慣れるため少しずつ記号表現を増やす。
【定義: 近傍の基本系】
E: 距離空間
A ⊂ E, A ≠ Φ: 距離空間の部分集合
O(A): A の近傍
λ ∈ L → U[λ] : A の近傍の族
∀O(A), ∃λ s.t. O(A) ⊃ U[λ] のとき、近傍の族 (U[λ]) を A の「近傍の基本系」と呼ぶ。
※ s.t. : such that
[命題]
N を(0を含まない)自然数とし、a を距離空間 E の任意の点とする。このとき、開球の族 n ∈ N → B(a; 1/n) は、{a} の近傍の基本系である。
[証明]
O(a) を a の任意の近傍とする。近傍の定義より、
U(a) ⊂ O(a)
となる開集合 U(a) が存在する。開集合の定義により、
B(a; r) ⊂ U(a)
となるある実数 r > 0 が存在する。アルキメデスの公理から、1/n ≦ r を満たすある自然数 n が存在するので
B(a; 1/n) ⊂ B(a; r) ⊂ U(a) ⊂ O(a)
となる。O(a) は {a} の任意の近傍であったので
∀O(a), ∃n∈ N s.t. B(a; 1/n) ⊂ O(a)
となる。したがって、開球の族 (B(a; 1/n)) は、{a} の近傍の基本系である。 //