Skip to content
Journals Garden

手筋: sup による中間値定理と「中間値の個数」不変量 (Ex IV.10.9)

  • 手筋: sup による中間値定理と「中間値の個数」不変量 (Ex IV.10.9) #Card
    • 連結性（第XIII章）もコンパクト性（第VIII章）も未導入の段階で、円周 $\rho$ と区間 $\mu$ が同相でないことを示す手筋は？

Back

Section titled “Back”

部品1: IVT の sup 証明（完備性だけで済む）. $\varphi: [u,v] \to \mathbb{R}$ 連続、$\varphi(u) < c < \varphi(v)$ なら $$\theta^* := \sup{\theta \in [u,v] : \varphi(\theta) \leq c}$$ が存在し（$\mathbb{R}$ の相対完備性、Example I.3.9）、ε-δ 連続性で $\varphi(\theta^) < c$ も $> c$ も sup 性と矛盾 → $\varphi(\theta^) = c$。使うのは sup の存在と cards/topology/continuity-epsilon-delta のみ。

部品2: 中間値の実現回数は同相不変. 同相 $h \in H(\rho, \mu)$ があれば、各値 $c \in [0,1]$ の実現点数 $\mathrm{card}, h^-(c)$ は 1（単射）。しかし円周では $0 = h^-(0)$ と $1 = h^-(1)$ の間に2つの弧があり、パラメータ化 $\varphi = h \circ e$（$e(\theta) = (\cos\theta, \sin\theta)$、始収束の普遍性で連続）に IVT を弧ごとに適用すると $\tfrac12$ が2回実現される——単射性と矛盾。ゆえに $\rho \not\approx \mu$（Ex IV.10.9）。

射程:

  • 「値の実現回数」「点を除いた残りの形」は初等的な同相不変量の原型（連結性導入後は「$\mathbb{S}$ は1点抜いても連結、$[0,1]$ は内点を抜くと分断」で一行になる）。
  • IVT 自体は分布関数（CDF）が中間値をとること・分位点（quantile）の存在・確率積分変換の骨格。sup 構成は測度論の「inf/sup で最適な点・集合を捕まえる」議論（Dynkin 系論法の極大元など）の初等版。

Lean

Section titled “Lean”

Mathlib: intermediate_value_Icc（順序位相＋条件完備束で一般化されている）。円と区間の非同相は Circle と Set.Icc の間に Homeomorph が無いこととして、通常 ConnectedSpace 系（Homeomorph.connectedSpace）で示す。