🚀 go-pugleaf

In article <SATOSHI.93Mar9193044@whale.math.ryukoku.ac.jp> satoshi@whale.math.ryukoku.ac.jp (Satoshi Kobayashi) writes:


$@;VB<!wF|Bg$G$9!#(J

$@EDJU7/$NEj9F$r$&$C$+$j>C$7$F$7$^$C$?$N$G!"$3$A$i$K%U%)%m!<(J
$@$7$^$9!#(J


$@>.(J$@NS(J> |$@EDJU(J> $@$9$k$H!$(Jd$@$N0l0U@-$+(J
$@>.NS(J> |$@EDJU(J> $@$i!$(JAFA$@$O$`$7$m(JF$@$N$h$&$J$b$N$NHsB8:_$r<gD%$7$F$$$k!%(J
$@>.NS(J> |
$@>.NS(J> |$@$H$$$&$N$,8m$j$G$3$3$GHsB8:_$,$o$+$k$N$O(J
$@>.NS(J> |	  $@=89gB2(J{b_r|r$@$O<B?t(J}$@$G!$(Jb_r={b_s|s$@$O(Jr$@$h$j(J$@Bg$-$J<B?t(J}
$@>.NS(J> |	  $@$H$J$k$b$N(J
$@>.NS(J> |$@$G$7$?!%!J:#EY$O9g$C$F$$$FM_$7$$$J$"!%!K(J
$@>.NS(J>
$@>.NS(J>$@$$$$$(!"$3(J$@$&$$$&$N$bB8:_$7$^$9!#<B:]!"A0$K=q$+$l$F$$$?$h$&$K!"<B?t$N=8(J

$@M>7W$J$3$H$G$9$,!"EDJU7/$,9M$($F$$$k$b$N(J$@$OA0$+$i$NOC$NN.$l(J
$@$G$O!"(J b_r=b_s $@$J$i$P(J r=s $@$H$J$k$b$N$G$7$g$&!#(J
$@$3$l$J$i$P!"@5$7$$!#(J

$@>.NS(J>$@$b$A$m$s(J$@!"(JAFA $@$G$O!"(JCollapsing Lemma $@$H0c$C$F!"%0%i%U$,(J extensional $@$@(J
$@>.NS(J>$@$H$$$&2>Dj$rCV$+$J$$$N$G!"%0%i%U$,(J \in $@4X78$HF17?$K$J$k$H$O8B$i$J$$$o(J
$@>.NS(J>$@$1$G$9$,!"I,MW$J$i!"%0%i%U$rE,Ev$JF1CM4X78$G3d$C$F$D$V$7$F(J extensional
$@>.NS(J>$@$K$7$F$*$$$F$+$i$d$l$P$$$$$o$1$G$9!#$3$3$G!"E,Ev$H$$$C$?$N$O!"@53N$K$O!"(J
$@>.NS(J>$@F1CM4X78(J$@$G3d$C$?;~$K(J extensional $@$K$J$k$h$&$J:G>.$NF1CM4X78$G3d$k$o$1(J
$@>.NS(J>$@$G$9!#(J
$@>.NS(J>


$@$3$3$G$$$&(J $@%0%i%U(J (G,R) $@$,(J extensional $@$G$"$k$H$O!"<!$N$3(J
$@$H$@$H;W$$$^$9!#(J 

a,b in G $@$N(J R $@$K$+$s$9$k(J $@?d0\E*JDJq$r$=$l$>(J$@$l(Jcl(a), cl(b)
$@$H$7$?$H$-!"(J R $@$N(J cl(a), cl(b) $@$X$N@)8B$,(J"$@%0%i%U$H$7$F(J"$@F17?(J
$@$J$i$P!"(Ja=b $@$G$"$k!#(J

$@>.NS(J>$@$G!"<B?t$H$=$N>e$NBg>.4X78$r%0%i%U$H9M$($?;~!"$3$l$O(J extensional $@$G$J(J
$@>.NS(J>$@$$$N$G$9$,!">e$G8@$C$?$h$&(J$@$K$7$F$D$V$7$F(J extensional $@$K$9$k$H!"(J1$@E@$H(J1
$@>.NS(J>$@8D$N%k!<%W$@$1$+$i$J$k%0%i%U$K$J$j$^$9!#$3$&9M$($k$H(J$@!"(Jd $@$H$7$F!"A4$F$N(J
$@>.NS(J>$@<B?t$K(J $@$5$C$-$N(J \Omega $@$rBP1~$5$;$k$b$N$r$H$l$P$h$$!"$H$$$&$3$H$OG<F@(J
$@>.NS(J>$@$7(J$@$d$9$$$H;W$$$^$9!#(J

$@IaDL(J extensional $@$H$$$&$H$-$O!"(J{x : xRa}={x : xRb} $@$J$i$P(J
a=b $@$r;X$9$H;W$&$N$G!"$3(J$@$N2r<a$N2<$G$O<B?t$N=89g$O(J 
extensional $@$@$1$l$I$b!"%0%i%U$H$7$F$O$=$&$G$O$J$$$H$$$&$3(J
$@$H$G$7$g$&!#(J

extensional $@$J%0%i%U$@$1$r9M$($l$PNI$$$H$$$&$N$O!"(JAFA $@$K$*(J
$@$1$k<LA|(J d $@$N0l0U@-$H!"301d@-8xM}(J (axiom of extensionality)
$@$+$i$N5"7k$@$H;W$$$^$9!#(J


--
$@F|K\Bg3XM}9)3XIt?t3X2J(J
	$@;VB<(J $@N)Lp(J
tel:03-3259-0943 e-mail:shimura@cst.nihon-u.ac.jp