命題
E を実数体または複素数体上の局所凸空間とする。
E が樽型空間(>>617)であるためには E の任意の下半連続(過去スレ008の113)
な半ノルム(過去スレ008の458)が連続であることが必要十分である。

証明
E を樽型空間とし、p を E の任意の下半連続な半ノルムとする。
B = { x ∈ E | p(x) ≦ 1 } は過去スレ008の516より凸集合である。
B が吸収的かつ平衡的であることは明らかである。
p は下半連続だから過去スレ008の114より B は閉集合である。
よって B は樽である。E は樽型空間だから B は 0 の近傍である。
>>570 より p は連続である。

逆に E の任意の下半連続な半ノルムが連続であるとする。
B を E における樽とする。
>>570 より E の下半連続な半ノルム p で
B = { x ∈ E | p(x) ≦ 1 } となるものが一意に存在する。
p は連続であるから >>570 より B は 0 の近傍である。
証明終