Mercurial > hg > Members > kono > Proof > ZF-in-agda
view fig/ord-od-mapping.svg @ 710:d20ba4b64ef3
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 14 Jul 2022 06:00:18 +0900 |
parents | 4cbcf71b09c4 |
children |
line wrap: on
line source
<?xml version="1.0" encoding="UTF-8" standalone="no"?> <!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"> <svg xmlns:xl="http://www.w3.org/1999/xlink" xmlns:dc="http://purl.org/dc/elements/1.1/" version="1.1" xmlns="http://www.w3.org/2000/svg" viewBox="37 -5 449 664" width="449" height="664"> <defs> <font-face font-family="Helvetica Neue" font-size="22" 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"> <font-face-src> <font-face-name name="HelveticaNeue"/> </font-face-src> </font-face> <font-face font-family="Helvetica Neue" font-size="14" 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"> <font-face-src> <font-face-name name="HelveticaNeue"/> </font-face-src> </font-face> <font-face font-family="Hiragino Sans" font-size="14" 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"> <font-face-src> <font-face-name name="HiraginoSans-W3"/> </font-face-src> </font-face> <marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-1 -4 10 8" markerWidth="10" markerHeight="8" color="black"> <g> <path d="M 8 0 L 0 -3 L 0 3 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/> </g> </marker> </defs> <metadata> Produced by OmniGraffle 7.12.1 <dc:date>2020-07-16 05:02:42 +0000</dc:date> </metadata> <g id="Canvas_1" fill-opacity="1" fill="none" stroke-opacity="1" stroke-dasharray="none" stroke="none"> <title>Canvas 1</title> <rect fill="white" x="37" y="-5" width="449" height="664"/> <g id="Canvas_1: Layer 1"> <title>Layer 1</title> <g id="Graphic_18"> <path d="M 159 49 L 186.21835 171 L 213.4367 49 Z" fill="white"/> <path d="M 159 49 L 186.21835 171 L 213.4367 49 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> </g> <g id="Graphic_17"> <path d="M 159 171 L 186.21835 293 L 213.4367 171 Z" fill="white"/> <path d="M 159 171 L 186.21835 293 L 213.4367 171 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> </g> <g id="Graphic_16"> <path d="M 159 293 L 186.21835 415 L 213.4367 293 Z" fill="white"/> <path d="M 159 293 L 186.21835 415 L 213.4367 293 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> </g> <g id="Graphic_15"> <path d="M 159 415 L 186.21835 537 L 213.4367 415 Z" fill="white"/> <path d="M 159 415 L 186.21835 537 L 213.4367 415 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> </g> <g id="Graphic_12"> <circle cx="186.21835" cy="16.5" r="6.50001038636233" fill="black"/> <circle cx="186.21835" cy="16.5" r="6.50001038636233" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> </g> <g id="Graphic_6"> <text transform="translate(155.245 553)" fill="black"> <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="21">Ordinal</tspan> </text> </g> <g id="Graphic_5"> <text transform="translate(289.326 536)" fill="black"> <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="21">Hereditarily Ordinal</tspan> <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="47.674" y="47.616">Definable</tspan> </text> </g> <g id="Graphic_20"> <text transform="translate(341.767 34)" fill="black"> <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="14210855e-21" y="13">max OD = all</tspan> </text> </g> <g id="Graphic_21"> <text transform="translate(289.326 509.608)" fill="black"> <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">empty</tspan> </text> </g> <g id="Graphic_22"> <text transform="translate(42 .10800171)" fill="black"> <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="23.261" y="13">Ordinal</tspan> <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="29.392">max != Ordinal</tspan> </text> </g> <g id="Graphic_25"> <text transform="translate(211.755 509.608)" fill="black"> <tspan font-family="Hiragino Sans" font-size="14" font-weight="300" fill="black" x="0" y="12">φ</tspan> </text> </g> <g id="Line_27"> <line x1="127" y1="535" x2="484.894" y2="535" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> </g> <g id="Graphic_34"> <circle cx="333.5" cy="16.5" r="6.50001038636232" fill="black"/> <circle cx="333.5" cy="16.5" r="6.50001038636232" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> </g> <g id="Line_40"> <line x1="372.3718" y1="630.664" x2="246.9" y2="630.664" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> </g> <g id="Line_39"> <line x1="188" y1="622.218" x2="365.575" y2="622.218" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> </g> <g id="Graphic_38"> <text transform="translate(253.792 599.232)" fill="black"> <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">non-order preserving</tspan> </text> </g> <g id="Graphic_37"> <text transform="translate(260.471 636.664)" fill="black"> <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">order preserving</tspan> </text> </g> <g id="Line_41"> <line x1="107" y1="356" x2="107" y2="274.47422" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> </g> <g id="Graphic_44"> <text transform="translate(45.888 318.13017)" fill="black"> <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="4973799e-19" y="13">larger</tspan> </text> </g> <g id="Line_46"> <line x1="330.222" y1="370" x2="346.15924" y2="273.84283" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> </g> <g id="Graphic_45"> <text transform="translate(352.771 318.13017)" fill="black"> <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="2.072" y="13">defined by </tspan> <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="29.392">or included</tspan> </text> </g> <g id="Line_47"> <line x1="330.222" y1="450" x2="330.222" y2="375.9664" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> </g> <g id="Line_48"> <line x1="347.778" y1="474.9336" x2="347.778" y2="400.9" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> </g> <g id="Line_49"> <line x1="339" y1="507.9336" x2="339" y2="433.9" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> </g> <g id="Line_50"> <line x1="322.762" y1="209.0664" x2="331.45437" y2="153.77986" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> </g> <g id="Line_51"> <line x1="343.222" y1="243.9336" x2="343.222" y2="169.9" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> </g> <g id="Line_52"> <line x1="322.762" y1="307" x2="322.762" y2="218.9664" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> </g> <g id="Line_53"> <line x1="347.778" y1="264.07607" x2="362.74265" y2="216.44483" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> </g> <g id="Line_54"> <line x1="330.222" y1="366.0664" x2="324.0025" y2="316.82197" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> </g> <g id="Graphic_55"> <text transform="translate(107 610.272)" fill="black"> <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">Total order</tspan> </text> </g> <g id="Graphic_56"> <text transform="translate(395 614.522)" fill="black"> <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="17053026e-20" y="13">Partial order</tspan> </text> </g> <g id="Graphic_57"> <text transform="translate(253.792 509.608)" fill="black"> <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="7274181e-19" y="13">=</tspan> </text> </g> <g id="Line_58"> <line x1="343.222" y1="151.9668" x2="342.36764" y2="93.89893" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> </g> <g id="Graphic_59"> <text transform="translate(357.433 89)" fill="black"> <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="1.946" y="13">HOD has </tspan> <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="7.133" y="29.392">no max</tspan> </text> </g> </g> </g> </svg>