:: Some Properties of Functions Modul and Signum
:: by Jan Popio{\l}ek
::
:: Received June 21, 1989
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines |. ABSVALUE:def 1 :
theorem Th1: :: ABSVALUE:1
theorem :: ABSVALUE:2
canceled;
theorem :: ABSVALUE:3
canceled;
theorem :: ABSVALUE:4
canceled;
theorem :: ABSVALUE:5
canceled;
theorem :: ABSVALUE:6
canceled;
theorem :: ABSVALUE:7
theorem :: ABSVALUE:8
canceled;
theorem :: ABSVALUE:9
theorem :: ABSVALUE:10
canceled;
theorem :: ABSVALUE:11
theorem :: ABSVALUE:12
theorem :: ABSVALUE:13
canceled;
theorem :: ABSVALUE:14
theorem :: ABSVALUE:15
theorem :: ABSVALUE:16
canceled;
theorem :: ABSVALUE:17
canceled;
theorem :: ABSVALUE:18
canceled;
theorem :: ABSVALUE:19
canceled;
theorem :: ABSVALUE:20
theorem :: ABSVALUE:21
theorem :: ABSVALUE:22
canceled;
theorem :: ABSVALUE:23
theorem :: ABSVALUE:24
theorem :: ABSVALUE:25
theorem :: ABSVALUE:26
:: deftheorem Def2 defines sgn ABSVALUE:def 2 :
theorem :: ABSVALUE:27
canceled;
theorem :: ABSVALUE:28
canceled;
theorem :: ABSVALUE:29
canceled;
theorem :: ABSVALUE:30
canceled;
theorem :: ABSVALUE:31
theorem :: ABSVALUE:32
theorem Th33: :: ABSVALUE:33
theorem :: ABSVALUE:34
theorem Th35: :: ABSVALUE:35
theorem :: ABSVALUE:36
theorem :: ABSVALUE:37
theorem Th38: :: ABSVALUE:38
theorem Th39: :: ABSVALUE:39
theorem :: ABSVALUE:40
theorem :: ABSVALUE:41
theorem :: ABSVALUE:42
theorem :: ABSVALUE:43
theorem :: ABSVALUE:44
theorem :: ABSVALUE:45