:: Uniform Boundedness Principle
:: by Hideki Sakurai , Hisayoshi Kunimune and Yasunari Shidama
::
:: Received October 9, 2007
:: Copyright (c) 2007 Association of Mizar Users
theorem Th1: :: LOPBAN_5:1
theorem :: LOPBAN_5:2
:: deftheorem defines Ball LOPBAN_5:def 1 :
theorem Th3: :: LOPBAN_5:3
theorem Th4: :: LOPBAN_5:4
theorem Th5: :: LOPBAN_5:5
:: deftheorem Def2 defines # LOPBAN_5:def 2 :
theorem Th6: :: LOPBAN_5:6
theorem Th7: :: LOPBAN_5:7
theorem :: LOPBAN_5:8