Mercurial > hg > Members > kono > Proof > ZF-in-agda
view fig/address-of-HOD.svg @ 632:1b57a07d7604
Added tag release for changeset 1150b006059b
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 20 Jun 2022 18:47:37 +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="253.785 161.5 248.185 537.116" width="248.185" height="537.116"> <defs> <marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-1 -3 6 6" markerWidth="6" markerHeight="6" color="black"> <g> <path d="M 3.7333333 0 L 0 -1.4 L 0 1.4 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/> </g> </marker> <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> <marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker_2" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-5 -3 6 6" markerWidth="6" markerHeight="6" color="black"> <g> <path d="M -3.7333333 0 L 0 1.4 L 0 -1.4 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/> </g> </marker> <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> </defs> <metadata> Produced by OmniGraffle 7.12.1 <dc:date>2020-07-16 09:18:05 +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="253.785" y="161.5" width="248.185" height="537.116"/> <g id="Canvas_1: Layer 1"> <title>Layer 1</title> <g id="Graphic_17"> <path d="M 262.54 407 L 289.75835 529 L 316.9767 407 Z" fill="white"/> <path d="M 262.54 407 L 289.75835 529 L 316.9767 407 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> </g> <g id="Line_22"> <path d="M 411.04 513.5 C 399.34904 489.1891 344.94662 458.1271 312.2266 439.7944" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> </g> <g id="Graphic_19"> <path d="M 262.54 163 L 289.75835 285 L 316.9767 163 Z" fill="white"/> <path d="M 262.54 163 L 289.75835 285 L 316.9767 163 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> </g> <g id="Graphic_18"> <path d="M 262.54 285 L 289.75835 407 L 316.9767 285 Z" fill="white"/> <path d="M 262.54 285 L 289.75835 407 L 316.9767 285 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> </g> <g id="Graphic_16"> <path d="M 262.54 529 L 289.75835 651 L 316.9767 529 Z" fill="white"/> <path d="M 262.54 529 L 289.75835 651 L 316.9767 529 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> </g> <g id="Graphic_15"> <ellipse cx="410.04" cy="512.5" rx="14.5000231695775" ry="82.5001318269065" fill="white"/> <ellipse cx="410.04" cy="512.5" rx="14.5000231695775" ry="82.5001318269065" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> </g> <g id="Graphic_13"> <circle cx="294.04" cy="215.5" r="6.50001038636234" fill="black"/> <circle cx="294.04" cy="215.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> </g> <g id="Graphic_11"> <circle cx="294.04" cy="338.5" r="6.50001038636235" fill="black"/> <circle cx="294.04" cy="338.5" r="6.50001038636235" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> </g> <g id="Graphic_10"> <circle cx="294.04" cy="429.5" r="6.50001038636236" fill="black"/> <circle cx="294.04" cy="429.5" r="6.50001038636236" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> </g> <g id="Graphic_9"> <circle cx="294.04" cy="458.5" r="6.50001038636234" fill="black"/> <circle cx="294.04" cy="458.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> </g> <g id="Graphic_8"> <circle cx="289.75835" cy="559.5" r="6.50001038636231" fill="black"/> <circle cx="289.75835" cy="559.5" r="6.50001038636231" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> </g> <g id="Graphic_7"> <text transform="translate(258.785 667)" 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_6"> <text transform="translate(367 608)" fill="black"> <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="37.07" y="21">HOD</tspan> <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="47.616">such as (x,y)</tspan> </text> </g> <g id="Graphic_4"> <circle cx="289.75835" cy="183.5" r="6.50001038636233" fill="black"/> <circle cx="289.75835" cy="183.5" r="6.50001038636233" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> </g> <g id="Line_21"> <path d="M 394.8927 484.52356 C 373.0247 446.2235 335.43026 385.45883 310.8905 355.36405" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> </g> <g id="Line_23"> <path d="M 432.15203 479.32975 C 465.39396 437.59087 508.5818 403.685 494 365 C 475.7518 316.58818 367.02 260.6628 300.54 222" marker-start="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="12.0,12.0" stroke-width="3"/> </g> <g id="Line_24"> <path d="M 432.5173 470.00093 C 444.1753 446.3428 445.478 433.10376 433 400 C 415.3925 353.28783 364.2836 345.6657 300.99565 310.45614" marker-start="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> </g> <g id="Graphic_12"> <circle cx="294.04" cy="306.5" r="6.50001038636234" fill="black"/> <circle cx="294.04" cy="306.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> </g> <g id="Graphic_25"> <text transform="translate(373 207.608)" fill="black"> <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="15.309" y="13">The address of</tspan> <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="5755396e-19" y="29.392">HOD has a freedom</tspan> </text> </g> </g> </g> </svg>