src/HOL/Limits.thy
 changeset 70803 2d658afa1fc0 parent 70723 4e39d87c9737 child 70804 4eef7c6ef7bf
equal inserted replaced
70802:160eaf566bcb 70803:2d658afa1fc0
`   777 `
`   777 `
`   778 lemma tendsto_mult_right: "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. (f x) * c) \<longlongrightarrow> l * c) F"`
`   778 lemma tendsto_mult_right: "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. (f x) * c) \<longlongrightarrow> l * c) F"`
`   779   for c :: "'a::topological_semigroup_mult"`
`   779   for c :: "'a::topological_semigroup_mult"`
`   780   by (rule tendsto_mult [OF _ tendsto_const])`
`   780   by (rule tendsto_mult [OF _ tendsto_const])`
`   781 `
`   781 `
`   782 lemma real_tendsto_mult_left_iff:`
`   782 lemma tendsto_mult_left_iff:`
`   783    "c \<noteq> 0 \<Longrightarrow> tendsto(\<lambda>x. c * f x) (c * l) F \<longleftrightarrow> tendsto f l F" for c :: real`
`   783    "c \<noteq> 0 \<Longrightarrow> tendsto(\<lambda>x. c * f x) (c * l) F \<longleftrightarrow> tendsto f l F" for c :: "'a::{topological_semigroup_mult,field}"`
`   784   by (auto simp: tendsto_mult_left dest: tendsto_mult_left [where c = "1/c"])`
`   784   by (auto simp: tendsto_mult_left dest: tendsto_mult_left [where c = "1/c"])`
`   785 `
`   785 `
`   786 lemma real_tendsto_mult_right_iff:`
`   786 lemma tendsto_mult_right_iff:`
`   787    "c \<noteq> 0 \<Longrightarrow> tendsto(\<lambda>x. f x * c) (l * c) F \<longleftrightarrow> tendsto f l F" for c :: real`
`   787    "c \<noteq> 0 \<Longrightarrow> tendsto(\<lambda>x. f x * c) (l * c) F \<longleftrightarrow> tendsto f l F" for c :: "'a::{topological_semigroup_mult,field}"`
`   788   by (simp add: mult.commute real_tendsto_mult_left_iff)`
`   788   by (auto simp: tendsto_mult_right dest: tendsto_mult_left [where c = "1/c"])`
`   789 `
`   789 `
`   790 lemma lim_const_over_n [tendsto_intros]:`
`   790 lemma lim_const_over_n [tendsto_intros]:`
`   791   fixes a :: "'a::real_normed_field"`
`   791   fixes a :: "'a::real_normed_field"`
`   792   shows "(\<lambda>n. a / of_nat n) \<longlonglongrightarrow> 0"`
`   792   shows "(\<lambda>n. a / of_nat n) \<longlonglongrightarrow> 0"`
`   793   using tendsto_mult [OF tendsto_const [of a] lim_1_over_n] by simp`
`   793   using tendsto_mult [OF tendsto_const [of a] lim_1_over_n] by simp`