{"width":"100%","author_name":"jurupapa","height":"190","url":"https://maxima.hatenablog.jp/entry/2024/02/01/000800","type":"rich","blog_title":"Maxima \u3067\u7db4\u308b\u6570\u5b66\u306e\u65c5","published":"2024-02-01 00:08:00","image_url":"https://cdn-ak.f.st-hatena.com/images/fotolife/j/jurupapa/20240131/20240131233530.jpg","blog_url":"https://maxima.hatenablog.jp/","title":"-\u6570\u5b66- Lean4\u306e\u304a\u52c9\u5f37 \u3000\u5b58\u5728\u91cf\u5316\u5b50 \u2203","author_url":"https://blog.hatena.ne.jp/jurupapa/","description":"\u30b4\u30fc\u30eb\u306b\u5b58\u5728\u91cf\u5316\u5b50\u304c\u5165\u3063\u3066\u3044\u308b\u5834\u5408\u3001\u5b58\u5728\u91cf\u5316\u5b50\u304c\u3064\u3044\u305f\u5909\u6570\u306b\u5024\u3092\u5165\u308b\u3053\u3068\u3067\u30b4\u30fc\u30eb\u306e\u8ad6\u7406\u5f0f\u3092\u8a3c\u660e\u3059\u308b\u3053\u3068\u304c\u3067\u304d\u307e\u3059\u3002use\u30bf\u30af\u30c6\u30a3\u30af\u3092\u4f7f\u3046\u3068\u3001\u300c\u3053\u306e\u5024\u3092\u4f7f\u3048\u300d\u3068\u3044\u3046\u3053\u3068\u304c\u3067\u304d\u307e\u3059\u3002\u4f8b\u3048\u3070\u3053\u3093\u306a\u611f\u3058\u3067\u3059\u3002 example : \u2203 x : \u211d, 2 < x \u2227 x < 3 := by use 5 / 2 -- \u22a2 2 < 5 / 2 \u2227 5 / 2 < 3 norm_num -- No goals \u30b4\u30fc\u30eb\u306e\u8ad6\u7406\u5f0f\u306e\u610f\u5473\u306f\u300c2\u3088\u308a\u5927\u304d\u304f\u30663\u3088\u308a\u5c0f\u3055\u3044\u5b9f\u6570x\u304c\u5b58\u5728\u3059\u308b\u300d\u3067\u3059\u3002\u307e\u3042\u5f53\u305f\u308a\u524d\u3067\u3059\u304c\u3069\u3046\u3084\u3063\u3066\u8a3c\u660e\u3059\u308b\u304b\u3067\u3059\u3002\u3053\u306e\u5834\u5408x\u304c$\\frac{5}{2}$\u3067\u3042\u308c\u3070\u3053\u306e\u4e0d\u7b49\u5f0f\u306f\u78ba\u304b\u306b\u6210\u7acb\u3059\u308b\u306e\u3067\u3001x\u304c\u5b58\u5728\u2026","version":"1.0","provider_name":"Hatena Blog","provider_url":"https://hatena.blog","html":"<iframe src=\"https://hatenablog-parts.com/embed?url=https%3A%2F%2Fmaxima.hatenablog.jp%2Fentry%2F2024%2F02%2F01%2F000800\" title=\"-\u6570\u5b66- Lean4\u306e\u304a\u52c9\u5f37 \u3000\u5b58\u5728\u91cf\u5316\u5b50 \u2203 - Maxima \u3067\u7db4\u308b\u6570\u5b66\u306e\u65c5\" class=\"embed-card embed-blogcard\" scrolling=\"no\" frameborder=\"0\" style=\"display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;\"></iframe>","categories":["\u6570\u5b66"]}