Continuous Map (連続写像) (Section IV.2)
- Continuous Map (連続写像) (Section IV.2) #Card
- $f : X \to Y$ is continuous at $x$ (from $\xi$ to $\tau$) if for every filter $\mathcal{F}$: $x \in \lim_\xi \mathcal{F} \implies f(x) \in \lim_\tau f[\mathcal{F}]$; continuous ($f \in C(\xi, \tau)$) if so at each $x$.
Let $\xi$, $\tau$ be convergences on $X$, $Y$. A map $f : X \to Y$ is continuous at $x$ (from $\xi$ to $\tau$) if for every filter $\mathcal{F}$ on $X$, $$x \in \lim_\xi \mathcal{F} \implies f(x) \in \lim_\tau f[\mathcal{F}];$$ continuous if this holds for each $x \in X$. $C(\xi, \tau)$ = the set of continuous maps from $\xi$ to $\tau$. 同値な形: $f(\lim_\xi \mathcal{F}) \subset \lim_\tau f[\mathcal{F}]$。
- 「連続 = 収束を保つ」。$f[\mathcal{F}]$ はフィルター基底だが (III.1.2) の規約で意味を持つ。
- $\xi \geq \theta \iff i_X \in C(\xi, \theta)$（恒等写像の連続性が順序そのもの）。
- $C(\iota_X, \tau) = Y^X = C(\xi, o_Y)$（離散から・混沌へは全て連続）；$C(o_X, \iota_Y)$ = 定値写像全体。
位相の場合 Continuous f；点での連続は ContinuousAt f x = Tendsto f (𝓝 x) (𝓝 (f x))。一般の ConvergenceSpace では Notes/ChapterIV.lean : Continuous