ご回答誠に有難うございます。
>>> ∪_{g ∈ S'} graph(g) = graph(∪_{g ∈ S'} g)
>>> の ∪_{g ∈ S'} g に定義をきちんと与えましょう.
>> ∪_{g ∈ S'} g :={(a,b)∈A×B;∃g∈S' such that g(a)=b} です。
> ∪_{g ∈ S'} g は写像である筈です. 写像については,
proj_A(∪_{g∈S'}graph(g))が定義域で
proj_B(∪_{g∈S'}graph(g))が値域です。
従って,proj_A(∪_{g∈S'}gの定義は
∀a∈proj_A(∪_{g∈S'}graph(g))に対して,∃g∈S';a∈dom(g)
(∵もし∀g∈S',aはdom(g)に含まれないとすると
即ち(a,g(a))は∪_{g∈S'}graph(g)に含まれないとすると
(∵graphの定義),それでaはproj_A(∪_{g∈S'}graph(g))に含まれない。
従ってこれはa∈proj_A(∪_{g∈S'}graph(g))に矛盾)
更にたとえ∃g,h∈S';a∈dom(g),a∈dom(h)であってもg(a)=h(a)
(∵今S'は全順序なのでg≦hかg≧h,即ちgraph(g)⊂graph(h)かgraph(g)⊃graph(h)
従って{∪_{g∈S'}g)(a)}は単集合),
で一応,写した先が1つの元になっているのでこれで写像の定義としてみたいのですが
これは苦し紛れですね。
それとも∪_{g∈S'}(g):=∪_{g∈S'}graph(g)と強引に定義してみたりしたのですが,,,
> どんな集合の上で定義されていて, どんな集合に値を取り,
> それぞれの元の行き先がどのようにして決まるか, を
> 述べないと定義を与えたことにはなりません.
> {(a,b)∈A×B;∃g∈S' such that g(a)=b} では意味不明です.
すいません。
> ここで求められているのは, ∪_{g ∈ S'} graph(g) が
> ある写像の graph となっていることを示すことです.
つまり,∪_{g∈S'}gのgraphになっている事ですよね。
> 先ず, A × B の部分集合が, A のある部分集合上で定義された,
> B のある部分集合に値を取る, ある写像の graph になる為の
> 必要十分条件は何であるかを述べた上で,
fをA'⊂AからB'⊂Bへの写像とするとf=graph(f)が必要十分条件だと思います。
> ∪_{g ∈ S'} graph(g) が, 実際, その条件を満足することを
> 示すことです.
うーんと,
∪_{g∈S'}graph(g)=∪_{g∈S'}(g) (∵∪_{g∈S'}(g):=∪_{g∈S'}graph(g))
=graph(∪_{g∈S'}g) (∵∪_{g∈S'}gは写像より)
とかしてみたのですが。。。
> 実の所, 更に, その写像は全単射でなければなりませんから,
> 先ず, A × B の部分集合が, A のある部分集合上で定義された,
> B のある部分集合に値を取る, ある全単射写像の graph になる為の
> 必要十分条件は何であるかを述べた上で,
> ∪_{g ∈ S'} graph(g) が, 実際, その条件を満足することを
> 示す必要があります.
A×B⊃A'×B'においてMap(A',B')∋f:全単射
⇔
∀a∈proj_A(graph(f)),∃!f(a)∈proj_B(graph(g))ですかね。
>>> 更にそれが S の元であることも示しましょう.
>>> その証明で S' が chain であるという条件が
>>> 使われていることを確かめましょう.
>> 例えば、f,g∈S'ならf≦g(かf≧g)となる(∵S'は鎖なので全順序集合)。
>> よってgraph(f)⊂graph(g)(かgraph(f)⊃graph(g))となる(∵≦の定義)。
>> その時,f≦f∪g,つまり全単射fのグラフは全単射f∪gにのグラフに吸収された形と
>> なるので
> ここまでは良いとしても,
そうですか。
>> ∪_{g ∈ S'} gも全単射となる。
> これには理由が示されていません.
常に全単射のgraphに吸収され続けるのでその極限のgraph全単射かなあと思ったのですが
論理的にはどのように示せばいいのかわかりませんでした。
>> 従って,∪_{g ∈ S'} g ∈S (∵Sの定義)
>> となるのですね。
> 貴方の議論は論理的でありません.
申し訳ありません。
Fnews-brouse 1.9(20180406) -- by Mizuno, MWE <mwe@ccsf.jp>
GnuPG Key ID = ECC8A735
GnuPG Key fingerprint = 9BE6 B9E9 55A5 A499 CD51 946E 9BDC 7870 ECC8 A735