Lower Semicontinuity of Relations (関係の下半連続性) (Definitions IV.9.1 / IV.9.3)
- Lower Semicontinuity of Relations (関係の下半連続性) (Definitions IV.9.1 / IV.9.3) #Card
- A relation $R \subset X \times Y$ is lower semicontinuous at $(x,y)$ if $x \in \lim_\xi \mathcal{F}$ entails a filter $\mathcal{G}$ with $y \in \lim_\tau \mathcal{G}$ and $\mathcal{F} \geq R^-[\mathcal{G}]$.
Let $R \subset X \times Y$, $\xi$ on $X$, $\tau$ on $Y$. $R$ is lower semicontinuous at $(x, y)$ if $x \in \lim_\xi \mathcal{F}$ entails the existence of a filter $\mathcal{G}$ such that $y \in \lim_\tau \mathcal{G}$ and $$\mathcal{F} \geq R^-[\mathcal{G}]. \tag{IV.9.1}$$
- $\xi, \tau$ が前位相なら $V_\xi(x) \geq R^-[V_\tau(y)]$ に簡約。
- 写像は特別な場合（Proposition IV.9.2）: $R_x = {f(x)}$ のとき、$f$ が $x$ で連続 $\iff R$ が $(x, f(x))$ で下半連続。
- 抽象版（Def IV.9.3）: $R \in C(\mathcal{F}, \mathcal{G})$ $:\iff$ (IV.9.1)、equivalently $R[\mathcal{F}] \geq \mathcal{G}$——「フィルターからフィルターへの下半連続性」。
位相の場合 LowerSemicontinuous（実数値）；集合値版は Mathlib では Continuity 系にない（E. Michael の理論）