-
Notifications
You must be signed in to change notification settings - Fork 0
/
Las_subsucesiones_tienen_el_mismo_limite_que_la_sucesion.thy
83 lines (75 loc) · 3.58 KB
/
Las_subsucesiones_tienen_el_mismo_limite_que_la_sucesion.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
(* Las_subsucesiones_tienen_el_mismo_limite_que_la_sucesion.thy
-- Las subsucesiones tienen el mismo límite que la sucesión
-- José A. Alonso Jiménez
-- Sevilla, 1 de septiembre de 2021
-- ------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
-- Para extraer una subsucesión se aplica una función de extracción que
-- conserva el orden; por ejemplo, la subsucesión
-- uₒ, u₂, u₄, u₆, ...
-- se ha obtenido con la función de extracción \<phi> tal que \<phi>(n) = 2*n.
--
-- En Isabelle/HOL, se puede definir que \<phi> es una función de extracción
-- por
-- definition extraccion :: "(nat \<Rightarrow> nat) \<Rightarrow> bool" where
-- "extraccion \<phi> \<longleftrightarrow> (\<forall> n m. n < m \<longrightarrow> \<phi> n < \<phi> m)"
-- que v es una subsucesión de u por
-- definition subsucesion :: "(nat \<Rightarrow> real) \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> bool"
-- where "subsucesion v u \<longleftrightarrow> (\<exists> \<phi>. extraccion \<phi> \<and> v = u \<circ> \<phi>)"
-- y que a es un límite de u por
-- definition limite :: "(nat \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> bool"
-- where "limite u a \<longleftrightarrow> (\<forall>\<epsilon>>0. \<exists>N. \<forall>k\<ge>N. \<bar>u k - a\<bar> < \<epsilon>)"
--
-- Demostrar que las subsucesiones de una sucesión convergente tienen el
-- mismo límite que la sucesión.
-- ------------------------------------------------------------------ *)
theory Las_subsucesiones_tienen_el_mismo_limite_que_la_sucesion
imports Main HOL.Real
begin
definition extraccion :: "(nat \<Rightarrow> nat) \<Rightarrow> bool" where
"extraccion \<phi> \<longleftrightarrow> (\<forall> n m. n < m \<longrightarrow> \<phi> n < \<phi> m)"
definition subsucesion :: "(nat \<Rightarrow> real) \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> bool"
where "subsucesion v u \<longleftrightarrow> (\<exists> \<phi>. extraccion \<phi> \<and> v = u \<circ> \<phi>)"
definition limite :: "(nat \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> bool"
where "limite u a \<longleftrightarrow> (\<forall>\<epsilon>>0. \<exists>N. \<forall>k\<ge>N. \<bar>u k - a\<bar> < \<epsilon>)"
(* En la demostración se usará el siguiente lema *)
lemma aux :
assumes "extraccion \<phi>"
shows "n \<le> \<phi> n"
proof (induct n)
show "0 \<le> \<phi> 0" by simp
next
fix n assume HI : "n \<le> \<phi> n"
then show "Suc n \<le> \<phi> (Suc n)"
using assms extraccion_def
by (metis Suc_leI lessI order_le_less_subst1)
qed
(* Demostración *)
lemma
assumes "subsucesion v u"
"limite u a"
shows "limite v a"
proof (unfold limite_def; intro allI impI)
fix \<epsilon> :: real
assume "\<epsilon> > 0"
then obtain N where hN : "\<forall>k\<ge>N. \<bar>u k - a\<bar> < \<epsilon>"
using assms(2) limite_def by auto
obtain \<phi> where h\<phi>1 : "extraccion \<phi>" and h\<phi>2 : "v = u \<circ> \<phi>"
using assms(1) subsucesion_def by auto
have "\<forall>k\<ge>N. \<bar>v k - a\<bar> < \<epsilon>"
proof (intro allI impI)
fix k
assume "N \<le> k"
also have "... \<le> \<phi> k"
by (simp add: aux h\<phi>1)
finally have "N \<le> \<phi> k" .
have "\<bar>v k - a\<bar> = \<bar>u (\<phi> k) - a\<bar>"
using h\<phi>2 by simp
also have "\<dots> < \<epsilon>"
using hN \<open>N \<le> \<phi> k\<close> by simp
finally show "\<bar>v k - a\<bar> < \<epsilon>" .
qed
then show "\<exists>N. \<forall>k\<ge>N. \<bar>v k - a\<bar> < \<epsilon>"
by auto
qed
end