フロワーマップ（写像）の定義
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、マップ（写像）の定義を知っている。
ターゲットコンテキスト
- 読者は、フロワーマップ（写像）の定義を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(*fl\): \(: [0, \infty) \to \mathbb{N}, r \mapsto Max (\{n \in \mathbb{N} \vert n \le r\})\)
//
コンディションたち:
//
2: 注
\(fl\)はいくつかのプロパティたちを満たすこと、を見よう。
1): 各\(r \in [0, \infty)\)に対して、\(fl (r) \le r\)、そして、もしも、\(r \in \mathbb{N}\)である場合、そしてその場合に限って、\(fl (r) = r\)、なぜなら、\(r = n + r'\)、ここで、\(0 \le r' \lt 1\)、そして、\(fl (r) = fl (n + r') = n\)、そして、\(fl (r) = n \le n + r' = r\); もしも、\(r \in \mathbb{N}\)である場合、\(r' = 0\)、そして、\(fl (r) = n = r\)、そして、もしも、\(fl (r) = r\)である場合、\(n = r\)、したがって、\(r \in \mathbb{N}\)。
2): 各\(r \in [0, \infty)\)に対して、\(fl \circ fl (r) = fl (r)\)、なぜなら、\(fl (r) \in \mathbb{N}\)および1)が適用される。
3): \(r \le r'\)を満たす各\(r, r' \in [0, \infty)\)に対して、\(fl (r) \le fl (r')\)、しかし、必ずしも、\(r \lt r'\)は\(fl (r) \lt fl (r')\)を含意しない、なぜなら、もしも、\(r \le r'\)である場合、\(\{n \in \mathbb{N} \vert n \le r\} \subseteq \{n \in \mathbb{N} \vert n \le r'\}\)および任意のパーシャリーオーダードセット（半順序集合）、任意のサブセット（部分集合）、当該サブセット（部分集合）の任意のサブセット（部分集合）に対して、もしも、当該サブセット（部分集合）のインフィマム（下限）および当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）が存在する場合、当該サブセット（部分集合）のインフィマム（下限）は当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）に等しいかそれより小さく、もしも、当該サブセット（部分集合）のサプリマム（上限）および当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）が存在する場合、当該サブセット（部分集合）のサプリマム（上限）は当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）に等しいかそれより大きいという命題が適用される: 当該マキシマム（最大）たちは当該サプリマム（上限）たちである; もしも、\(r \lt r'\)である場合、もしも、\(r = 1.1\)および\(r' = 1.2\)である場合、\(fl (r) = 1 = fl (r')\)、したがって、"\(fl (r) \lt fl (r')\)"は必ずしも成立しない。
4): 各\(r \in [0, \infty)\)に対して、\(r \lt fl (r + 1)\)、なぜなら、\(r = n + r'\)、ここで、\(0 \le r' \lt 1\)、そして、\(fl (r + 1) = fl (n + 1 + r') = n + 1\)および\(n + r' \lt n + 1\)。
5): 各\(r, r' \in [0, \infty)\)に対して、もしも、\(fl (r) \le r'\)である場合、そしてその場合に限って、\(r \lt fl (r' + 1)\)、なぜなら、もしも、\(fl (r) \le r'\)であったら、もしも、\(fl (r' + 1) \le r\)であった場合、\(fl (r' + 1) = fl \circ fl (r' + 1) \le fl (r)\)、2)および3)によって、\(\le r'\)、4)に反する矛盾; もしも、\(r \lt fl (r' + 1)\)である場合、\(fl (r) \le r \lt fl (r' + 1)\)、1)によって、しかし、\(r' = n + r''\)、ここで、\(0 \le r'' \lt 1\)、そして、\(fl (r' + 1) = fl (n + 1 + r'') = n + 1\)、したがって、\(fl (r) \lt n + 1\)、しかし、\(fl (r) \in \mathbb{N}\)であるから、\(fl (r) \le n \lt n + 1\)、そして、\(fl (r) \le n \le n + r'' = r'\)。
