{"type":"rich","author_url":"https://blog.hatena.ne.jp/m-hiyama-memo/","url":"https://m-hiyama-memo.hatenablog.jp/entry/20161214/1481709485","published":"2016-12-14 18:58:05","categories":["Mizar","\u30c0\u30e1\u51fa\u3057"],"blog_url":"https://m-hiyama-memo.hatenablog.jp/","author_name":"m-hiyama-memo","provider_url":"https://hatena.blog","height":"190","version":"1.0","html":"<iframe src=\"https://hatenablog-parts.com/embed?url=https%3A%2F%2Fm-hiyama-memo.hatenablog.jp%2Fentry%2F20161214%2F1481709485\" title=\"\u60c5\u5831\u691c\u7d22\u6cd5 - (\u4fdd\u5b58\u7528) \u6a9c\u5c71\u6b63\u5e78\u306e\u30ad\u30de\u30a4\u30e9\u98fc\u80b2\u8a18 \u30e1\u30e2\u7de8\" class=\"embed-card embed-blogcard\" scrolling=\"no\" frameborder=\"0\" style=\"display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;\"></iframe>","title":"\u60c5\u5831\u691c\u7d22\u6cd5","blog_title":"(\u4fdd\u5b58\u7528) \u6a9c\u5c71\u6b63\u5e78\u306e\u30ad\u30de\u30a4\u30e9\u98fc\u80b2\u8a18 \u30e1\u30e2\u7de8","provider_name":"Hatena Blog","width":"100%","image_url":null,"description":"\u30e1\u30bf\u60c5\u5831 - \u6a9c\u5c71\u6b63\u5e78\u306e\u30ad\u30de\u30a4\u30e9\u98fc\u80b2\u8a18 \u30e1\u30e2\u7de8 \u3042\u305f\u308a\u304b\u3089\uff1ahttp://fm.mizar.org/contents.html \u304b\u3089MML ID\u3067\u63a2\u3059\u3002 \u4f8b Volume 1, 1990 http://fm.mizar.org/1990-1/pdf1-1/tarski.pdf \u4f8b Volume 2, 1991 http://fm.mizar.org/1991-2/pdf2-3/oppcat_1.pdf \u30c6\u30f3\u30d7\u30ec\u306f\u3001http://fm.mizar.org/{\u5e74}-{\u5dfb}/pdf{\u5dfb}-{\u53f7}/{\u5c0f\u6587\u5b57ID} \u3002\u30e9\u30a4\u30d6\u30e9\u30ea\u53ce\u9332\u7248\u306f\u304a\u305d\u3089\u304f http://mizar.org/JFM/pdf/{\u5c0f\u6587\u5b57\u2026"}