Mercurial > hg > Members > kono > Proof > ZF-in-agda

view fig/address-of-HOD.svg @ 752:2be90b90deb3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dead end
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 23 Jul 2022 17:19: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="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>