:: RUSUB_4 semantic presentation :: Showing IDV graph ... (Click the Palm Trees again to close it)
theorem Th1: :: RUSUB_4:1 :: Showing IDV graph ... (Click the Palm Tree again to close it)
Lm1:
for X, x being set st x in X holds
(X \ {x}) \/ {x} = X
Lm2:
for X, x being set st not x in X holds
X \ {x} = X
theorem Th2: :: RUSUB_4:2 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem Def1 defines finite-dimensional RUSUB_4:def 1 :
:: deftheorem Def2 defines finite-dimensional RUSUB_4:def 2 :
theorem Th3: :: RUSUB_4:3 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: RUSUB_4:4 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th5: :: RUSUB_4:5 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th6: :: RUSUB_4:6 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th7: :: RUSUB_4:7 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem Def3 defines dim RUSUB_4:def 3 :
theorem Th8: :: RUSUB_4:8 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th9: :: RUSUB_4:9 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th10: :: RUSUB_4:10 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: RUSUB_4:11 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th12: :: RUSUB_4:12 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: RUSUB_4:13 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: RUSUB_4:14 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th15: :: RUSUB_4:15 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: RUSUB_4:16 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: RUSUB_4:17 :: Showing IDV graph ... (Click the Palm Tree again to close it)
Lm3:
for V being finite-dimensional RealUnitarySpace
for n being Nat st n <= dim V holds
ex W being strict Subspace of V st dim W = n
theorem :: RUSUB_4:18 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem Def4 defines Subspaces_of RUSUB_4:def 4 :
theorem :: RUSUB_4:19 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: RUSUB_4:20 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: RUSUB_4:21 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem Def5 defines Affine RUSUB_4:def 5 :
theorem Th22: :: RUSUB_4:22 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: RUSUB_4:23 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem defines Up RUSUB_4:def 6 :
:: deftheorem defines Up RUSUB_4:def 7 :
theorem :: RUSUB_4:24 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th25: :: RUSUB_4:25 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem Def8 defines Subspace-like RUSUB_4:def 8 :
theorem Th26: :: RUSUB_4:26 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: RUSUB_4:27 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: RUSUB_4:28 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: RUSUB_4:29 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: RUSUB_4:30 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: RUSUB_4:31 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem defines + RUSUB_4:def 9 :
theorem :: RUSUB_4:32 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th33: :: RUSUB_4:33 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: RUSUB_4:34 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem defines + RUSUB_4:def 10 :
theorem Th35: :: RUSUB_4:35 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th36: :: RUSUB_4:36 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: RUSUB_4:37 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: RUSUB_4:38 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: RUSUB_4:39 :: Showing IDV graph ... (Click the Palm Tree again to close it)