\input /home/pasky/school/fastex/lib.tex

\theorem{}{Bolzano---Weieistrassova v�ta}{

	Z ka�d� omezen� posloupnosti lze vybrat konvergentn� podposloupnost.


\proof{

	Nech� $\{a_{n}\}$ je omezen� posloupnost. Pak definujme
	$$ A = \limsup_{n\to\infty} a_{n} $$

	Plat�, �e $A \in \real$, nebo� $\{a_{n}\}$ je omezen�, tedy
	$$b_{1} = \sup_{n\in\nat}(a_{n}) \in \real$$
	$$c_{1} = \inf_{n\in\nat}(a_{n}) \in \real$$
	$$c_{1} \le c_{n} \le b_{n} \le b_{1}\qquad \forall n \in \nat$$

	Definujeme mno�inu:
	$$ M_{1} \defined \{ j\in\nat : a_{j} \in [A-1,A+1] \} \not= \emptyset $$
	$$ m_{1} \defined \min M_{1} $$
	(index prvn�ho bodu v p�sku $A-1,A+1$).

	Nech� jsou definov�na $n_{1},\ldots{},n_{k-1}$. Pak definujeme:
	$$ M_{k} \defined \{ j\in\nat,\ j > n_{k-1} : a_{j} \in [A-1/2^k, A+1/2^k] \} $$
	$$ n_{k} \defined \min M_{k} $$

	Takto definuji nekone�nou posloupnost index� $\{n_{k}\}_{k\in\nat}$.
	T�m z�sk�v�m vybranou posloupnost
	$$d_{k} = a_{n_{k}}\qquad k\in\nat$$

	Tvrd�m, �e $\lim_{k\to\infty} d_{k} = A$.
	Zvolme $\eps > 0$, pak $\existss k_{0}$ takov�, �e
	$${1/2^k} < \eps\qquad \forall k \ge k_{0}$$
	Tedy $|d_{k}-A| < \eps$ pro $k \ge k_{0}$, tedy
	$$\lim_{k\to\infty} d_{k} = A$$

	\qed

}

}


\theorem{}{Bolzano---Cauchyova v�ta}{

	Posloupnost $\{a_{n}\}$ m� vlastn� limitu, pr�v� kdy� plat� tzv. Bolzano---Cauchyova podm�nka:

	$$ \textbox{Pro ka�d� $\eps>0$ existuje $n_{0} \in \nat$ takov�, �e:} $$
	$$ |a_{m}-a_{n}| < \eps \qquad \forall m,n\in\nat\quad (m,n \ge n_{0}) $$

\penalty-100

\proof{

\proofrightimpl{

	Zvol�me $\eps > 0$, pak $\existss n_{0}$ takov�, �e pro $\forall n \ge n_{0}$ plat�: $$|A-a_{n}| < \eps/2$$

	Tedy pro $\forall m,n \ge n_{0}$:
	$$ |a_{m}-a_{n}| = |a_{m}-A+A-a_{n}| \le |a_{m}-A| + |a_{n}-A| < \eps/2 + \eps/2 = \eps $$

}

\proofleftimpl{
	Zvol�me $\eps > 0$, pak $\existss n_{0}$ takov�, �e pro $\forall n \ge n_{0}$ plat�: $$|a_{m}-a_{n}| < \eps$$

	Speci�ln� pro $m=n_{0}$:
	$$ a_{n_{0}} - \eps < a_{n} < a_{n_{0}} + \eps \qquad (\forall n \ge n_{0}) $$

	$$ a_{n_{0}} - \eps < \liminf a_{n} \le \limsup a_{n} < a_{n_{0}} + \eps \qquad (\forall \eps>0) $$

	$$ \liminf_{n\to\infty} a_{n} = \limsup_{n\to\infty} a_{n} \becauseof{\hbox{\ias{}{10}{}}}{\Rightarrow} \existss \lim a_{n} = \limsup a_{n} \in \real $$
}

	\qed

}

}

\bend
