{"author_name":"kururu_goedel","author_url":"https://blog.hatena.ne.jp/kururu_goedel/","blog_url":"https://kururu.hatenablog.com/","image_url":null,"type":"rich","html":"<iframe src=\"https://hatenablog-parts.com/embed?url=https%3A%2F%2Fkururu.hatenablog.com%2Fentry%2F2026%2F07%2F06%2F131637\" title=\"attribute\u3068\u304b\u305d\u306e\u4ed6\u306e\u516c\u7406\u3044\u304f\u3064\u304b\u3068\u304b - kururu_goedel\u2019s diary\" class=\"embed-card embed-blogcard\" scrolling=\"no\" frameborder=\"0\" style=\"display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;\"></iframe>","version":"1.0","blog_title":"kururu_goedel\u2019s diary","description":"attribute \u524d\u56de\u66f8\u3044\u305f\u901a\u308a\u3001\u4f8b\u3048\u3070 variable {V : Type*} [SetStructure V] [hV_Nonempty: Nonempty V] [hV_ZFC : V \u22a7\u2098* \ud835\udded\ud835\uddd9\ud835\uddd6]\u3068\u304b\u3057\u3066\u3084\u308b\u3068\u3001V\u306fZFC\u306e\u30e2\u30c7\u30eb\u3068\u3057\u3066\u632f\u308b\u821e\u3046\u3053\u3068\u306b\u306a\u308b\u3002\u305d\u308c\u306f\u3068\u3066\u3082\u826f\u3044\u306e\u3060\u3051\u308c\u3069\u3082\u3001Z.lean\u306fV \u22a7\u2098* \ud835\udded\u3068\u3044\u3046\u4eee\u5b9a\u306e\u3082\u3068\u306b\u66f8\u304b\u308c\u3066\u3044\u3066\u3001\u3053\u306eV \u22a7\u2098* \ud835\udded\ud835\uddd9\ud835\uddd6\u3068\u3044\u3046\u4eee\u5b9a\u3060\u3068\u81ea\u52d5\u7684\u306b\u306f\u9069\u7528\u3055\u308c\u306a\u3044\u3002\u307f\u305f\u3044\u3002\u4f8b\u3048\u3070\u3001\u3053\u308c\u306f[V \u22a7\u2098* \ud835\udded]\u3092\u6d88\u3059\u3068\u901a\u3089\u306a\u3044\u3002\u305d\u308c\u3069\u3053\u308d\u304b\u3001\u2205\u304c\u3053\u306e\u5834\u5408\u306a\u306b\u304b\u308f\u304b\u3089\u306a\u3044\u3068\u8a00\u3044\u51fa\u3059\u3002 example [V \u22a7\u2098* \ud835\udded] : IsEmpty (\u2205 :\u2026","width":"100%","provider_name":"Hatena Blog","categories":[],"provider_url":"https://hatena.blog","title":"attribute\u3068\u304b\u305d\u306e\u4ed6\u306e\u516c\u7406\u3044\u304f\u3064\u304b\u3068\u304b","height":"190","published":"2026-07-06 13:16:37","url":"https://kururu.hatenablog.com/entry/2026/07/06/131637"}