jurupapa https://blog.hatena.ne.jp/jurupapa/ Maxima で綴る数学の旅 https://maxima.hatenablog.jp/ 数学 ゴールに存在量化子が入っている場合、存在量化子がついた変数に値を入ることでゴールの論理式を証明することができます。useタクティクを使うと、「この値を使え」ということができます。例えばこんな感じです。 example : ∃ x : ℝ, 2 < x ∧ x < 3 := by use 5 / 2 -- ⊢ 2 < 5 / 2 ∧ 5 / 2 < 3 norm_num -- No goals ゴールの論理式の意味は「2より大きくて3より小さい実数xが存在する」です。まあ当たり前ですがどうやって証明するかです。この場合xが$\frac{5}{2}$であればこの不等式は確かに成立するので、xが存在… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fmaxima.hatenablog.jp%2Fentry%2F2024%2F02%2F01%2F000800" title="-数学- Lean4のお勉強 　存在量化子 ∃ - Maxima で綴る数学の旅" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> https://cdn-ak.f.st-hatena.com/images/fotolife/j/jurupapa/20240131/20240131233530.jpg Hatena Blog https://hatena.blog 2024-02-01 00:08:00 rich https://maxima.hatenablog.jp/entry/2024/02/01/000800 1.0 100%