POSTAGEM ORIGINAL:
Estou tentando mostrar o seguinte:
have "continuous_on {x. 0 < x} (λx. 12 * x⇧2 - 1)"
E eu gostaria de usar o seguinte lema:
thm continuous_on_diff
----------------------------------------------------------------------------------------------------------
Output:
⟦continuous_on ?s ?f; continuous_on ?s ?g⟧ ⟹ continuous_on ?s (λx. ?f x - ?g x)
Mas talvez essa não seja a forma correta, então tento isso:
have "continuous_on {x. 0 < x} (λx. (λw . 12 * w⇧2) x - (λw . 1)x)"
apply(subst continuous_on_diff)
Mas isso não funcionou, então deixei ainda mais explícito:
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}"])
Mas mesmo isso não funcionou, entretanto quando verifiquei o teorema:
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)
Parece ser exatamente o que eu quero. A única coisa que consigo pensar é que "subst" não é adequado para lidar com argumentos de estilo não equacional, e também não consigo fazer "rule" funcionar.
Qualquer ajuda é muito apreciada!
De forma semelhante, também estou lutando para provar:
"have continuous_on {x. 0 < x} ((*) 6)"
EDIT: Quando tornei as informações de digitação mais explícitas, como em:
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}"])
Isso tornou isso provável. Mas qual é a diferença?