原始帖子：
我试图展示以下内容：
have "continuous_on {x. 0 < x} (λx. 12 * x⇧2 - 1)"
我想使用以下引理：
thm continuous_on_diff
----------------------------------------------------------------------------------------------------------
Output:
⟦continuous_on ?s ?f; continuous_on ?s ?g⟧ ⟹ continuous_on ?s (λx. ?f x - ?g x)
但也许这不是正确的形式所以我尝试这个：
have "continuous_on {x. 0 < x} (λx. (λw . 12 * w⇧2) x - (λw . 1)x)"
apply(subst continuous_on_diff)
但这不起作用所以我使它更加明确：
have "continuous_on {x. 0 < x} (λx. (λw . 12 * w⇧2) x - (λw . 1)x)"
apply(subst continuous_on_diff[where f = "(λw . 12 * w⇧2)" and g= "(λw . 1)" and s = "{x. 0 < x}"])
然而，这仍然不起作用，然而，当我检查定理时：
thm continuous_on_diff[where f = "(λw . 12 * w⇧2)" and g = "(λw . 1)" and s = "{x. 0 < x}"]
-------------------------------------------------------------------------------------------
Output:
⟦continuous_on {x. 0 < x} (λw. 12 * w⇧2); continuous_on {x. 0 < x} (λw. 1)⟧ ⟹ continuous_on {x. 0 < x} (λx. 12 * x⇧2 - 1)
这似乎正是我想要的。我唯一能想到的是“subst”不适合处理非等式风格的参数，而且我也无法让“rule”工作。
任何帮助都将不胜感激！
类似地，我也在努力证明：
"have continuous_on {x. 0 < x} ((*) 6)"
编辑：当我使输入信息更加明确时，例如：
have "continuous_on {x :: real. 0 < x} (λx. (λw . 12 * w⇧2) x - (λw . 1)x)"
apply(rule continuous_on_diff[where f = "(λw . 12 * w⇧2)" and g = "(λw . 1)" and s = "{x. 0 < x}"])
这使得它可证明。但是有什么区别呢？