Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison fig/Sets.svg @ 273:9ccf8514c323
add documents
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 11 Jan 2020 20:11:51 +0900 |
parents | |
children |
comparison
equal
deleted
inserted
replaced
272:985a1af11bce | 273:9ccf8514c323 |
---|---|
1 <?xml version="1.0" encoding="UTF-8" standalone="no"?> | |
2 <!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"> | |
3 <svg version="1.1" xmlns="http://www.w3.org/2000/svg" xmlns:xl="http://www.w3.org/1999/xlink" xmlns:dc="http://purl.org/dc/elements/1.1/" viewBox="26 93 572 303" width="572" height="303"> | |
4 <defs> | |
5 <font-face font-family="Hiragino Sans" font-size="18" panose-1="2 11 3 0 0 0 0 0 0 0" units-per-em="1000" underline-position="-75" underline-thickness="50" slope="0" x-height="545" cap-height="766" ascent="880.0018" descent="-120.00024" font-weight="300"> | |
6 <font-face-src> | |
7 <font-face-name name="HiraginoSans-W3"/> | |
8 </font-face-src> | |
9 </font-face> | |
10 <font-face font-family="Helvetica Neue" font-size="18" panose-1="2 0 5 3 0 0 0 2 0 4" units-per-em="1000" underline-position="-100" underline-thickness="50" slope="0" x-height="517" cap-height="714" ascent="951.9958" descent="-212.99744" font-weight="400"> | |
11 <font-face-src> | |
12 <font-face-name name="HelveticaNeue"/> | |
13 </font-face-src> | |
14 </font-face> | |
15 </defs> | |
16 <metadata> Produced by OmniGraffle 7.12.1 | |
17 <dc:date>2019-11-27 13:34:32 +0000</dc:date> | |
18 </metadata> | |
19 <g id="Canvas_1" stroke-dasharray="none" stroke="none" fill="none" stroke-opacity="1" fill-opacity="1"> | |
20 <title>Canvas 1</title> | |
21 <rect fill="white" x="26" y="93" width="572" height="303"/> | |
22 <g id="Canvas_1: Layer 1"> | |
23 <title>Layer 1</title> | |
24 <g id="Graphic_2"> | |
25 <text transform="translate(133 98.00003)" fill="black"> | |
26 <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="16">様々な集合</tspan> | |
27 </text> | |
28 </g> | |
29 <g id="Graphic_4"> | |
30 <text transform="translate(108 137.00001)" fill="black"> | |
31 <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="16">順序数の公理を満たすもの。自然数の延長</tspan> | |
32 </text> | |
33 </g> | |
34 <g id="Graphic_5"> | |
35 <text transform="translate(108 176)" fill="black"> | |
36 <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="16">一つ一つ増やす。無限回繰り返して、それを全部。</tspan> | |
37 <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="43.00002">また一つ一つ増やすを繰り返して得られるもの</tspan> | |
38 </text> | |
39 </g> | |
40 <g id="Graphic_6"> | |
41 <text transform="translate(108 233.696)" fill="black"> | |
42 <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="16">述語で定義されるものを集めるのを繰り返して作られるもの</tspan> | |
43 </text> | |
44 </g> | |
45 <g id="Graphic_7"> | |
46 <text transform="translate(108 281.99994)" fill="black"> | |
47 <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="16">順序数上の方程式を満たす順序数の集合</tspan> | |
48 <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="43.00002">階層化されていない</tspan> | |
49 </text> | |
50 </g> | |
51 <g id="Graphic_8"> | |
52 <text transform="translate(31.59 137.00001)" fill="black"> | |
53 <tspan font-family="Helvetica Neue" font-size="18" font-weight="400" fill="black" x="0" y="17">Ordinal</tspan> | |
54 </text> | |
55 </g> | |
56 <g id="Graphic_9"> | |
57 <text transform="translate(54.936 176)" fill="black"> | |
58 <tspan font-family="Helvetica Neue" font-size="18" font-weight="400" fill="black" x="0" y="17">V</tspan> | |
59 </text> | |
60 </g> | |
61 <g id="Graphic_10"> | |
62 <text transform="translate(53.23 281.99994)" fill="black"> | |
63 <tspan font-family="Helvetica Neue" font-size="18" font-weight="400" fill="black" x="0" y="17">OD</tspan> | |
64 </text> | |
65 </g> | |
66 <g id="Graphic_11"> | |
67 <text transform="translate(55.816 233.696)" fill="black"> | |
68 <tspan font-family="Helvetica Neue" font-size="18" font-weight="400" fill="black" x="8144596e-19" y="17">L</tspan> | |
69 </text> | |
70 </g> | |
71 <g id="Graphic_12"> | |
72 <text transform="translate(51.174 336)" fill="black"> | |
73 <tspan font-family="Helvetica Neue" font-size="18" font-weight="400" fill="black" x="2.502" y="17">Set </tspan> | |
74 </text> | |
75 </g> | |
76 <g id="Graphic_13"> | |
77 <text transform="translate(108 336)" fill="black"> | |
78 <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="16">型。集まりではなく、値の種類を区別する記号。’</tspan> | |
79 <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="43.00002">自身が値になると、一つLevelの高い型を持つ</tspan> | |
80 </text> | |
81 </g> | |
82 </g> | |
83 </g> | |
84 </svg> |