:: Circled Sets, Circled Hull, and Circled Family
:: by Fahui Zhai , Jianbing Cao and Xiquan Liang
::
:: Received August 30, 2005
:: Copyright (c) 2005 Association of Mizar Users
Lm1:
for V being non empty RLSStruct
for M, N being Subset of V
for x, y being VECTOR of V st x in M & y in N holds
x - y in M - N
theorem Th1: :: CIRCLED1:1
:: deftheorem Def1 defines circled CIRCLED1:def 1 :
theorem Th2: :: CIRCLED1:2
theorem Th3: :: CIRCLED1:3
theorem :: CIRCLED1:4
theorem :: CIRCLED1:5
theorem Th6: :: CIRCLED1:6
theorem :: CIRCLED1:7
theorem :: CIRCLED1:8
:: deftheorem Def2 defines Circled-Family CIRCLED1:def 2 :
:: deftheorem defines Cir CIRCLED1:def 3 :
theorem Th9: :: CIRCLED1:9
theorem :: CIRCLED1:10
theorem Th11: :: CIRCLED1:11
theorem Th12: :: CIRCLED1:12
theorem :: CIRCLED1:13
theorem Th14: :: CIRCLED1:14
theorem :: CIRCLED1:15
:: deftheorem Def4 defines circled CIRCLED1:def 4 :
theorem Th16: :: CIRCLED1:16
theorem Th17: :: CIRCLED1:17
theorem :: CIRCLED1:18
theorem Th19: :: CIRCLED1:19
theorem Th20: :: CIRCLED1:20
:: deftheorem defines circledComb CIRCLED1:def 5 :
:: deftheorem defines circledComb CIRCLED1:def 6 :
theorem :: CIRCLED1:21
theorem :: CIRCLED1:22
theorem :: CIRCLED1:23
theorem Th24: :: CIRCLED1:24
theorem Th25: :: CIRCLED1:25
theorem :: CIRCLED1:26
theorem :: CIRCLED1:27