Обговорення:Теорема Больцано — Веєрштрасса

Доповнення

Дополнение к статье «Bolzano-Weierstrass theorem»

$~t\vdash \quad \mathrm {f} :\mathbb {N} \mapsto \mathbb {R} \quad \land \quad \exists _{\{a,b\}\ \subseteq \ \mathbb {R} \ \land \ a\ \leq \ b}\ \forall _{n\ \in \ \mathbb {N} }\ (a\leq f_{n}\leq b)\quad \to$

$~\exists _{\mathrm {g} :\ \mathbb {N} \ \mapsto \ \mathbb {R} }\ (\forall _{m\ \in \ \mathbb {N} }\ \exists _{n\ \in \ \mathbb {N} }^{\{1\}}\ (g_{m}=f_{n})\quad \land \quad \forall _{n\ \in \ \mathbb {N} }\ \exists _{m\ \in \ \mathbb {N} }^{\{0,1\}}\ (g_{m}=f_{n})\quad \land \quad (\lim _{m\to \infty }g_{m})\in \mathbb {R} )$

Примечание

$~\mathrm {f} :\mathbb {N} \mapsto \mathbb {R}$ - последовательность вещественных чисел, то есть вещественная функция натурального аргумента.

$~\mathrm {f} :\mathbb {N} \mapsto \mathbb {R} \ \Leftrightarrow \ \mathrm {f} =\{\langle n,f_{n}\rangle |\quad \langle n,f_{n}\rangle \in \mathbb {N} \times \mathbb {R} \quad \land \ \quad f_{n}=f(n)\}$

$~\mathrm {f} :\mathbb {N} \mapsto \mathbb {R} \ \Leftrightarrow \ \mathrm {f} \subseteq \mathbb {N} \times \mathbb {R} \quad \land \quad \mathrm {f} \neq \varnothing \quad \land \quad \forall _{n\ \in \ \mathbb {N} }\ \exists _{x\ \in \ \mathbb {R} }^{\{1\}}\ (\langle n,x\rangle \in \mathrm {f} )$

$~\mathrm {f} \subseteq \mathbb {N} \times \mathbb {R} \ \Leftrightarrow \ \forall n\forall x\ (\langle n,x\rangle \in \mathrm {f} \ \to \ \langle n,x\rangle \in \mathbb {N} \times \mathbb {R} )$

$~\mathrm {f} \subseteq \mathbb {N} \times \mathbb {R} \ \Leftrightarrow \ \mathrm {f} \in {\mathcal {P}}(\mathbb {N} \times \mathbb {R} )$

$~{\mathcal {P}}(\mathbb {N} \times \mathbb {R} )$ - булеан (= множество всех подмножеств) декартового произведения $~\mathbb {N} \times \mathbb {R}$

$~\forall _{n\ \in \ \mathbb {N} }\ \exists _{x\ \in \ \mathbb {R} }^{\{1\}}(\langle n,x\rangle \in \mathrm {f} )\ \Leftrightarrow \ \forall n\ (n\in \mathbb {N} \to \exists ^{\{1\}}x\ (x\in \mathbb {R} \ \land \ \langle n,x\rangle \in \mathrm {f} )$

$~\exists ^{\{1\}}x\ (x\in \mathbb {R} \ \land \ \langle n,x\rangle \in \mathrm {f} )\ \Leftrightarrow \ \exists _{x\ \in \ \mathbb {R} }^{\{1,...\}}\ (\langle n,x\rangle \in \mathrm {f} )\quad \land \quad \exists _{x\ \in \ \mathbb {R} }^{\{0,1\}}\ (\langle n,x\rangle \in \mathrm {f} )$

$~\exists _{x\ \in \ \mathbb {R} }^{\{1,...\}}\ (\langle n,x\rangle \in \mathrm {f} )\ \Leftrightarrow \ \exists _{x\ \in \ \mathbb {R} }\ (\langle n,x\rangle \in \mathrm {f} )\ \Leftrightarrow \ \exists x\ (x\in \mathbb {R} \ \land \ \langle n,x\rangle \in \mathrm {f} )$

$~\exists _{x\ \in \ \mathbb {R} }^{\{0,1\}}\ (\langle n,x\rangle \in \mathrm {f} )\ \Leftrightarrow \ \forall x_{1}\forall x_{2}\ (\{x_{1},x_{2}\}\subseteq \mathbb {R} \ \ \land \ \ \{\langle n,x_{1}\rangle ,\ \langle n,x_{2}\rangle \}\subseteq \mathrm {f} \to x_{1}=x_{2})$

$~\{x_{1},x_{2}\}\subseteq \mathbb {R} \ \Leftrightarrow \ x_{1}\in \mathbb {R} \ \land \ x_{2}\in \mathbb {R}$

$~\{\langle n,x_{1}\rangle ,\ \langle n,x_{2}\rangle \}\subseteq \mathrm {f} \ \Leftrightarrow \ \langle n,x_{1}\rangle \in \mathrm {f} \ \land \ \langle n,x_{2}\rangle \in \mathrm {f}$

$~\exists _{\{a,b\}\ \subseteq \ \mathbb {R} \ \land \ a\ \leq \ b}\ \forall _{n\ \in \ \mathbb {N} }\ (a\leq f_{n}\leq b)$ - "якiсть" (an attribute or a property) последовательности $~\mathrm {f} :\mathbb {N} \mapsto \mathbb {R}$.

$~\mathrm {f} :\mathbb {N} \mapsto \mathbb {R} \ \land \ \exists _{\{a,b\}\ \subseteq \ \mathbb {R} \ \land \ a\ \leq \ b}\ \forall _{n\ \in \ \mathbb {N} }\ (a\leq f_{n}\leq b)$ - последовательность вещественных чисел ограничена снизу и сверху.

$~\exists _{\{a,b\}\ \subseteq \ \mathbb {R} \ \land \ a\ \leq \ b}\ \forall _{n\ \in \ \mathbb {N} }\ (a\leq f_{n}\leq b)\ \Leftrightarrow \ \exists a\exists b\ (\{a,b\}\subseteq \mathbb {R} \ \land \ a\leq b\ \land \ \forall n\ (n\in \mathbb {N} \to a\leq f_{n}\leq b))$

$~\{a,b\}\subseteq \mathbb {R} \ \Leftrightarrow \ a\in \mathbb {R} \ \land \ b\in \mathbb {R}$

$~a\leq f_{n}\leq b\ \Leftrightarrow \ a\leq f_{n}\ \land \ f_{n}\leq b$

Галактион 01:00, 20 серпня 2009 (UTC)