real-number

6熱

2答えて

私は実数のために定義された関係「未満」であるか疑問に思って。 Iは自然数（nat）ため、<は別の番号の（1+）後継Sであるつの番号の点で再帰的に定義することができることを理解します。実数についての多くのことがCoqでは公理であり、計算しないと聞きました。しかし、私は他のプロパティ/関係が導出することができるに基づいてCoqので実数のための公理の最小セットがあるかどうかを疑問に思って。特に（例え

3熱

1答えて

基礎学部計算のためのCoquelicotライブラリ

Coquelicotをmathcomp/SSreflectの上にインストールしました。私はまだ標準Coqを習得していなくても、非常に基本的な実際の分析を実行したいと思います。これが私の最初の補題です： Definition fsquare (x : R) : R := x^2. Lemma deriv_x2 : forall y, is_derive (fsquare) y (2 * y).