:: On Segre's Product of Partial Line Spaces
:: by Adam Naumowicz
::
:: Received May 29, 2000
:: Copyright (c) 2000 Association of Mizar Users
theorem Th1: :: PENCIL_1:1
theorem Th2: :: PENCIL_1:2
for
X being
set holds
( 2
c= card X iff ex
x,
y being
set st
(
x in X &
y in X &
x <> y ) )
theorem Th3: :: PENCIL_1:3
theorem Th4: :: PENCIL_1:4
theorem Th5: :: PENCIL_1:5
for
X being
set holds
( 3
c= card X iff ex
x,
y,
z being
set st
(
x in X &
y in X &
z in X &
x <> y &
x <> z &
y <> z ) )
theorem Th6: :: PENCIL_1:6
:: deftheorem Def1 defines are_collinear PENCIL_1:def 1 :
:: deftheorem Def2 defines closed_under_lines PENCIL_1:def 2 :
:: deftheorem Def3 defines strong PENCIL_1:def 3 :
:: deftheorem Def4 defines void PENCIL_1:def 4 :
:: deftheorem Def5 defines degenerated PENCIL_1:def 5 :
:: deftheorem Def6 defines with_non_trivial_blocks PENCIL_1:def 6 :
:: deftheorem Def7 defines identifying_close_blocks PENCIL_1:def 7 :
:: deftheorem Def8 defines truly-partial PENCIL_1:def 8 :
:: deftheorem Def9 defines without_isolated_points PENCIL_1:def 9 :
:: deftheorem defines connected PENCIL_1:def 10 :
:: deftheorem Def11 defines strongly_connected PENCIL_1:def 11 :
theorem Th7: :: PENCIL_1:7
Lm1:
ex S being TopStruct st
( S is strict & not S is empty & not S is void & not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
theorem Th8: :: PENCIL_1:8
Lm2:
ex S being TopStruct st
( S is strict & not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
:: deftheorem defines are_collinear PENCIL_1:def 12 :
:: deftheorem Def13 defines TopStruct-yielding PENCIL_1:def 13 :
:: deftheorem Def14 defines non-void-yielding PENCIL_1:def 14 :
:: deftheorem defines non-void-yielding PENCIL_1:def 15 :
:: deftheorem Def16 defines trivial-yielding PENCIL_1:def 16 :
:: deftheorem Def17 defines non-Trivial-yielding PENCIL_1:def 17 :
:: deftheorem defines non-Trivial-yielding PENCIL_1:def 18 :
:: deftheorem Def19 defines PLS-yielding PENCIL_1:def 19 :
:: deftheorem Def20 defines Segre-like PENCIL_1:def 20 :
theorem :: PENCIL_1:9
theorem :: PENCIL_1:10
theorem Th11: :: PENCIL_1:11
:: deftheorem Def21 defines indx PENCIL_1:def 21 :
theorem Th12: :: PENCIL_1:12
theorem Th13: :: PENCIL_1:13
:: deftheorem Def22 defines Segre_Blocks PENCIL_1:def 22 :
:: deftheorem defines Segre_Product PENCIL_1:def 23 :
theorem Th14: :: PENCIL_1:14
theorem Th15: :: PENCIL_1:15
theorem Th16: :: PENCIL_1:16
theorem Th17: :: PENCIL_1:17
theorem Th18: :: PENCIL_1:18
theorem :: PENCIL_1:19
theorem Th20: :: PENCIL_1:20
theorem Th21: :: PENCIL_1:21
theorem :: PENCIL_1:22
theorem Th23: :: PENCIL_1:23
theorem Th24: :: PENCIL_1:24
theorem Th25: :: PENCIL_1:25
theorem Th26: :: PENCIL_1:26
theorem Th27: :: PENCIL_1:27
theorem :: PENCIL_1:28
theorem :: PENCIL_1:29