Skip to content

Instantly share code, notes, and snippets.

@hatsugai
Created March 4, 2020 15:11
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save hatsugai/84b4567e8c138d1e21ca3a436fd7e6fc to your computer and use it in GitHub Desktop.
Save hatsugai/84b4567e8c138d1e21ca3a436fd7e6fc to your computer and use it in GitHub Desktop.
theory X imports Complex_Main begin
consts a :: "nat => real"
theorem
"k > 0 ==>
(ALL e. e > 0 --> (EX N1. (ALL n. n > N1 --> abs (a n - b) < e)))
= (ALL e. e > 0 --> (EX N2. (ALL n. n > N2 --> abs (a n - b) < k * e)))"
apply(rule iffI)
apply(rule allI)
apply(rule impI)
apply(drule_tac x="k * e" in spec)
apply(drule mp)
apply(simp)
apply(erule exE)
apply(rule_tac x="N1" in exI)
apply(rule allI)
apply(rule impI)
apply(drule_tac x="n" in spec)
apply(drule mp)
apply(simp)
apply(simp)
(**)
apply(rule allI)
apply(rule impI)
apply(drule_tac x="e / k" in spec)
apply(drule mp)
apply(simp)
apply(erule exE)
apply(rule_tac x="N2" in exI)
apply(rule allI)
apply(rule impI)
apply(drule_tac x="n" in spec)
apply(drule mp)
apply(simp)
apply(simp)
done
theorem
"k > 0 ==>
(ALL e. e > 0 --> (EX N1. n > N1 --> abs (a n - b) < e))
= (ALL e. e > 0 --> (EX N2. n > N2 --> abs (a n - b) < k * e))"
apply(rule iffI)
apply(rule allI)
apply(rule impI)
apply(drule_tac x="k * e" in spec)
apply(drule mp)
apply(simp)
apply(erule exE)
apply(rule_tac x="N1" in exI)
apply(rule impI)
apply(drule mp)
apply(simp)
apply(simp)
(**)
apply(rule allI)
apply(rule impI)
apply(drule_tac x="e / k" in spec)
apply(drule mp)
apply(simp)
apply(erule exE)
apply(rule_tac x="N2" in exI)
apply(rule impI)
apply(drule mp)
apply(simp)
apply(simp)
done
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment