伊莎貝爾的換人

Question

在很多論文中，你可以看到作者在方程中使用替代變量。例如，如果存在不等式「f（xy）> = g（xy）* z，作者簡單地寫出讓h =（xy），因此」f（h）> = g（h）* z「並繼續

要做到這一點在伊莎貝爾，我必須假設h =（xy），有沒有其他的方式做到這一點？我看着「讓」功能，但是做了完全不同的事情。

具體而言，我有：

lemma 
fixes f g :: "real⇒real" 
assumes "∀x∈S. ∀y∈S. f y - f x ≥ (y-x)*(g x)" 
shows "∀x∈S. ∀h. f (x+h) - g x ≥ h*(g x)" 

所以我又讓H = YX

我可以顯示這個引理如果我假定第在「∀h。 ∀x∈S。 ∀y∈S。 H = YX」這是正確的做法？

Answer 1

有各種可能性進行置換。

如果你有元量詞的一些說法，你可以只使用where或of要啓用量詞∀公式爲元FORALL的，比如，你可以使用rule_format然後，assms[rule_format, of x "h+x"]產量在你的榜樣式x ∈ S ⟹ x + h ∈ S ⟹ f (x + h) - f x >= (x + h - x) * g x

在這裏，您可以立即看到兩個問題：。首先- f x和- g x之間的差異，以及它的問題不保證x + h ∈ S。

或者，您也可以通過展開來執行替換，例如，使用def h = "x - y"，然後摺疊或展開h_def。