定義
>>385の μ_0 を μ の半有限部分と言う。