:: The First Mean Value Theorem for Integrals
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received October 30, 2007
:: Copyright (c) 2007 Association of Mizar Users
theorem Th1: :: MESFUNC7:1
theorem Th2: :: MESFUNC7:2
theorem Th3: :: MESFUNC7:3
theorem :: MESFUNC7:4
:: deftheorem MESFUNC7:def 1 :
canceled;
:: deftheorem Def2 defines multextreal MESFUNC7:def 2 :
Lm1:
1. is_a_unity_wrt multextreal
theorem Th5: :: MESFUNC7:5
:: deftheorem Def3 defines Product MESFUNC7:def 3 :
:: deftheorem defines |^ MESFUNC7:def 4 :
theorem Th6: :: MESFUNC7:6
theorem Th7: :: MESFUNC7:7
theorem Th8: :: MESFUNC7:8
theorem Th9: :: MESFUNC7:9
theorem Th10: :: MESFUNC7:10
:: deftheorem Def5 defines |^ MESFUNC7:def 5 :
theorem Th11: :: MESFUNC7:11
theorem Th12: :: MESFUNC7:12
theorem Th13: :: MESFUNC7:13
theorem Th14: :: MESFUNC7:14
theorem Th15: :: MESFUNC7:15
theorem Th16: :: MESFUNC7:16
theorem :: MESFUNC7:17
theorem Th18: :: MESFUNC7:18
theorem Th19: :: MESFUNC7:19
theorem Th20: :: MESFUNC7:20
theorem Th21: :: MESFUNC7:21
theorem :: MESFUNC7:22
theorem Th23: :: MESFUNC7:23
theorem Th24: :: MESFUNC7:24
theorem Th25: :: MESFUNC7:25
theorem :: MESFUNC7:26