Mantenimiento del Ascensor Qué Incluye

ed
qed

text \Uniqueness of the limit is straightforward.\

theorem lim_unique:
assumes «((x \ l) F) \ ((x \ m) F)»
shows «l = m»
proof –
have «\y > 0. \N. \n \ N. dist (x n) l < y" using assms(1) unfolding tendsto_def by auto moreover have "\y > 0. \N. \n \ N. dist (x n) m < y" using assms(2) unfolding tendsto_def by auto ultimately have "\y > 0. \N. \n \ N. dist l m < y" by (metis dist_triangle_lt) thus ?thesis unfolding tendsto_def by auto qed end subsection \Limits at positive infinity\

text \We define the limit at positive infinity of a
real-valued sequence, and prove a few basic theorems.\

context metric_space
begin

definition lim_infinity :: «(nat \ ‘a) \ ‘a \ bool»
where «lim_infinity x l \ (\y. \N. \n \ N. x n \ y)»

lemma lim_infinity_I:
assumes «\y. \N. \n \ N. x n \ y»
shows «(lim_infinity x l)»
using assms unfolding lim_infinity_def by auto

lemma lim_infinity_D:
assumes «(lim_infinity x l)» and «y > l»
shows «\N. \n \ N. x n \ y»
using assms unfolding lim_infinity_def by auto

theorem lim_infinity_const:
assumes «c \ l»
shows «(lim_infinity (\n. c) l)»
proof –
have «\y. \N. \n \ N. c \ y»
using assms by auto
thus ?thesis unfolding lim_infinity_def by auto
qed

end

subsection \Limits at negative infinity\

text \We define the limit at negative infinity of a
real-valued sequence, and prove a few basic theorems.\

context metric_space
begin

definition lim_minus_infinity :: «(nat \ ‘a) \ ‘a \ bool»
where «lim_minus_infinity x l \ (\y. \N. \n \ N. x n \ y)»

lemma lim_minus_infinity_I:
assumes «\y. \N. \n \ N. x n \ y»
shows «(lim_minus_infinity x l)»
using assms unfolding lim_minus_infinity_def by auto

lemma lim_minus_infinity_D:
assumes «(lim_minus_infinity x l)» and «y < l" shows "\N. \n \ N. x n \ y»
using assms unfolding lim_minus_infinity_def by auto

theorem lim_minus_infinity_const:
assumes «c \ l»
shows «(lim_minus_infinity (\n. c) l)»
proof –
have «\y. \N. \n \ N. c \ y»
using assms by auto
thus ?thesis unfolding lim_minus_infinity_def by auto
qed

Artículo relacionado: Duración de vida útil de un ascensor

end

subsection \Limit superior and inferior\

text \We define the limit superior and limit inferior
for a real-valued sequence, and prove a few basic theorems.\

context metric_space
begin

definition lim_sup :: «(nat \ ‘a) \ ‘a \ bool»
where «lim_sup x l \ (\y > l. \N. \n \ N. x n > y)»

lemma lim_sup_I:
assumes «\y. y > l \ \N. \n \ N. x n > y»
shows «(lim_sup x l)»
using assms unfolding lim_sup_def by auto

lemma lim_sup_D:
assumes «(lim_sup x l)» and «y > l»
shows «\N. \n \ N. x n > y»
using assms unfolding lim_sup_def by auto

definition lim_inf :: «(nat \ ‘a) \ ‘a \ bool»
where «lim_inf x l \ (\y < l. \N. \n \ N. x n < y)" lemma lim_inf_I: assumes "\y. y < l \ \N. \n \ N. x n < y" shows "(lim_inf x l)" using assms unfolding lim_inf_def by auto lemma lim_inf_D: assumes "(lim_inf x l)" and "y < l" shows "\N. \n \ N. x n < y" using assms unfolding lim_inf_def by auto end subsection \Limits in a topological space\

text \We define the limit of a sequence in a topological
space, and prove a few basic theorems.\

context topological_space
begin

definition tendsto :: «(‘a \ ‘b) \ ‘b \ bool»
where «tendsto f l \ (\U. open U \ l \ U \ (\N. \n \ N. f n \ U))»

lemma tendsto_I:
assumes «\U. open U \ l \ U \ \N. \n \ N. f n \ U»
shows «(tendsto f l)»
using assms unfolding tendsto_def by auto

lemma tendsto_D:
assumes «(tendsto f l)» and «open U» and «l \ U»
shows «\N. \n \ N. f n \ U»
using assms unfolding tendsto_def by auto

theorem tendsto_const:
shows «(tendsto (\n. c) c)»
proof –
have «\U. open U \ c \ U \ (\N. \n \ N. c \ U)»
by auto
thus ?thesis unfolding tendsto_def by auto
qed

end

subsection \Cauchy sequence\

text \We define the Cauchy property for a sequence
in a metric space, and prove a few basic theorems.\

context metric_space
begin

definition cauchy :: «(nat \ ‘a) \ bool»
where «cauchy x \ (\e > 0. \N. \m \ N. \n \ N. dist (x m) (x n) < e)"

Artículo relacionado: Reparar un ascensor dañado: Guía paso a paso

lemma cauchy_I: assumes "\e. e > 0 \ \N. \m \ N. \n \ N. dist (x m) (x n) < e" shows "(cauchy x)" using assms unfolding cauchy_def by auto lemma cauchy_D: assumes "(cauchy x)" and "e > 0″
shows «\N. \m \ N. \n \ N. dist (x m) (x n) < e" using assms unfolding cauchy_def by auto end subsection \Facts about limits\

text \We prove a few facts about the limits of sequences
in a metric space.\

context metric_space
begin

theorem lim_I:
assumes «\e. e > 0 \ \N. \n \ N. dist (x n) l < e" shows "(x \ l) F»
using assms unfolding tendsto_def by auto

theorem lim_D:
assumes «(x \ l) F» and «e > 0»
shows «\N. \n \ N. dist (x n) l < e" using assms unfolding tendsto_def by auto text \A constant sequence converges to its value.\

theorem lim_const:
shows «(\n. c) \ c»
proof –
have «\e > 0. \N. \n \ N. dist (c) (c) < e" by auto thus ?thesis unfolding tendsto_def by auto qed text \The limit of the sum of two sequences is the sum of their limits.\

theorem lim_add:
assumes «(x \ a) F» and «(y \ b) F»
shows «((\n. x n + y n) \ a + b) F»
proof –
have «\e > 0. \N. \n \ N. dist (x n + y n) (a + b) < e" proof - { fix e::real assume "e > 0″
moreover have «\M. \n \ M. dist (x n) a < e/2" using assms(1) \e > 0\ unfolding tendsto_def by auto
moreover have «\N. \n \ N. dist (y n) b < e/2" using assms(2) \e > 0\ unfolding tendsto_def by auto
ultimately have «\N. \n \ N. dist (x n + y n) (a + b) < e" using dist

¿Qué incluye el mantenimiento del ascensor?

Artículos relacionados:

Comparte conocimiento