:: PENCIL_4 semantic presentation begin theorem :: PENCIL_4:1 (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Num 3) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Bool "not" (Set (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))))) "holds" (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) ; theorem :: PENCIL_4:2 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Var "W")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "V"))))))) ; theorem :: PENCIL_4:3 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "V"))) "holds" (Bool (Set (Var "W")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")))))) ; theorem :: PENCIL_4:4 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "W"))) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")))))) ; theorem :: PENCIL_4:5 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "W"))) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")))) "holds" (Bool (Set (Var "W")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V"))))) ; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); let "W1", "W2" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); func :::"segment"::: "(" "W1" "," "W2" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_vectsp_5 :::"Subspaces"::: ) "V" ")" ) means :: PENCIL_4:def 1 (Bool "for" (Set (Var "W")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" "V" "holds" (Bool "(" (Bool (Set (Var "W")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool "W1" "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W"))) & (Bool (Set (Var "W")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" "W2") ")" ) ")" )) if (Bool "W1" "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" "W2") otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"segment"::: PENCIL_4:def 1 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_vectsp_5 :::"Subspaces"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W2")))) "implies" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k1_pencil_4 :::"segment"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" )) "iff" (Bool "for" (Set (Var "W")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "W")) ($#r2_hidden :::"in"::: ) (Set (Var "b5"))) "iff" (Bool "(" (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W"))) & (Bool (Set (Var "W")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W2"))) ")" ) ")" )) ")" ) ")" & "(" (Bool (Bool (Set (Var "W1")) "is" (Bool "not" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W2"))))) "implies" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k1_pencil_4 :::"segment"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" )) "iff" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ")" ))))); theorem :: PENCIL_4:6 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "," (Set (Var "W4")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W2"))) & (Bool (Set (Var "W3")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W4"))) & (Bool (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "W1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "W3")))) & (Bool (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "W4"))))) "holds" (Bool (Set ($#k1_pencil_4 :::"segment"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_pencil_4 :::"segment"::: ) "(" (Set (Var "W3")) "," (Set (Var "W4")) ")" ))))) ; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); let "W1", "W2" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); func :::"pencil"::: "(" "W1" "," "W2" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_vectsp_5 :::"Subspaces"::: ) "V" ")" ) equals :: PENCIL_4:def 2 (Set (Set "(" ($#k1_pencil_4 :::"segment"::: ) "(" "W1" "," "W2" ")" ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k2_vectsp_4 :::"(Omega)."::: ) "W1" ")" ) "," (Set "(" ($#k2_vectsp_4 :::"(Omega)."::: ) "W2" ")" ) ($#k2_tarski :::"}"::: ) )); end; :: deftheorem defines :::"pencil"::: PENCIL_4:def 2 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k2_pencil_4 :::"pencil"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_pencil_4 :::"segment"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "W1")) ")" ) "," (Set "(" ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "W2")) ")" ) ($#k2_tarski :::"}"::: ) )))))); theorem :: PENCIL_4:7 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "," (Set (Var "W4")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W2"))) & (Bool (Set (Var "W3")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W4"))) & (Bool (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "W1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "W3")))) & (Bool (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "W4"))))) "holds" (Bool (Set ($#k2_pencil_4 :::"pencil"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_pencil_4 :::"pencil"::: ) "(" (Set (Var "W3")) "," (Set (Var "W4")) ")" ))))) ; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); let "W1", "W2" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); let "k" be ($#m1_hidden :::"Nat":::); func :::"pencil"::: "(" "W1" "," "W2" "," "k" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "k" ($#k2_vectsp_9 :::"Subspaces_of"::: ) "V" ")" ) equals :: PENCIL_4:def 3 (Set (Set "(" ($#k2_pencil_4 :::"pencil"::: ) "(" "W1" "," "W2" ")" ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "(" "k" ($#k2_vectsp_9 :::"Subspaces_of"::: ) "V" ")" )); end; :: deftheorem defines :::"pencil"::: PENCIL_4:def 3 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k3_pencil_4 :::"pencil"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pencil_4 :::"pencil"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "(" (Set (Var "k")) ($#k2_vectsp_9 :::"Subspaces_of"::: ) (Set (Var "V")) ")" ))))))); theorem :: PENCIL_4:8 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W")) ($#r2_hidden :::"in"::: ) (Set ($#k3_pencil_4 :::"pencil"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "k")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W"))) & (Bool (Set (Var "W")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W2"))) ")" ))))) ; theorem :: PENCIL_4:9 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "," (Set (Var "W4")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W2"))) & (Bool (Set (Var "W3")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W4"))) & (Bool (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "W1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "W3")))) & (Bool (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "W4"))))) "holds" (Bool (Set ($#k3_pencil_4 :::"pencil"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_pencil_4 :::"pencil"::: ) "(" (Set (Var "W3")) "," (Set (Var "W4")) "," (Set (Var "k")) ")" )))))) ; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); let "k" be ($#m1_hidden :::"Nat":::); func "k" :::"Pencils_of"::: "V" -> ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" "k" ($#k2_vectsp_9 :::"Subspaces_of"::: ) "V" ")" ) means :: PENCIL_4:def 4 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" "V" "st" (Bool "(" (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W2"))) & (Bool (Set (Set "(" ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W1")) ")" ) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) "k") & (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set "k" ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k3_pencil_4 :::"pencil"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) "," "k" ")" )) ")" )) ")" )); end; :: deftheorem defines :::"Pencils_of"::: PENCIL_4:def 4 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" (Set (Var "k")) ($#k2_vectsp_9 :::"Subspaces_of"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k4_pencil_4 :::"Pencils_of"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "ex" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W2"))) & (Bool (Set (Set "(" ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W1")) ")" ) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "k"))) & (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k3_pencil_4 :::"pencil"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "k")) ")" )) ")" )) ")" )) ")" ))))); theorem :: PENCIL_4:10 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "V"))))) "holds" (Bool "not" (Bool (Set (Set (Var "k")) ($#k4_pencil_4 :::"Pencils_of"::: ) (Set (Var "V"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))))) ; theorem :: PENCIL_4:11 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set "(" ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W1")) ")" ) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "k"))) & (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set ($#k3_pencil_4 :::"pencil"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "Q")) ($#r2_hidden :::"in"::: ) (Set ($#k3_pencil_4 :::"pencil"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set (Var "Q")))) "holds" (Bool "(" (Bool (Set (Set (Var "P")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "Q"))) ($#r1_hidden :::"="::: ) (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "W1")))) & (Bool (Set (Set (Var "P")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "Q"))) ($#r1_hidden :::"="::: ) (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "W2")))) ")" ))))) ; theorem :: PENCIL_4:12 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1))))) ; theorem :: PENCIL_4:13 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))))) "holds" (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set "(" (Set (Var "W")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W")) ")" ) ($#k1_nat_1 :::"+"::: ) (Num 1))))))) ; theorem :: PENCIL_4:14 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set (Var "u"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "v")) "," (Set (Var "u")) ($#k7_domain_1 :::"}"::: ) ) "is" ($#v1_vectsp_7 :::"linearly-independent"::: ) ) & (Bool (Set (Set (Var "W")) ($#k2_vectsp_5 :::"/\"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "v")) "," (Set (Var "u")) ($#k7_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "V"))))) "holds" (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set "(" (Set (Var "W")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "v")) "," (Set (Var "u")) ($#k7_domain_1 :::"}"::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W")) ")" ) ($#k1_nat_1 :::"+"::: ) (Num 2))))))) ; theorem :: PENCIL_4:15 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W2")))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set "(" ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W1")) ")" ) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "k"))) & (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))))) "holds" (Bool (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k3_pencil_4 :::"pencil"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "k")) ")" ))))))) ; theorem :: PENCIL_4:16 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W2")))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set "(" ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W1")) ")" ) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "k"))) & (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool "not" (Bool (Set ($#k3_pencil_4 :::"pencil"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "k")) ")" ) "is" ($#v1_zfmisc_1 :::"trivial"::: ) )))))) ; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); let "k" be ($#m1_hidden :::"Nat":::); func :::"PencilSpace"::: "(" "V" "," "k" ")" -> ($#v1_pre_topc :::"strict"::: ) ($#l1_pre_topc :::"TopStruct"::: ) equals :: PENCIL_4:def 5 (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "(" "k" ($#k2_vectsp_9 :::"Subspaces_of"::: ) "V" ")" ) "," (Set "(" "k" ($#k4_pencil_4 :::"Pencils_of"::: ) "V" ")" ) "#)" ); end; :: deftheorem defines :::"PencilSpace"::: PENCIL_4:def 5 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k5_pencil_4 :::"PencilSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "(" (Set (Var "k")) ($#k2_vectsp_9 :::"Subspaces_of"::: ) (Set (Var "V")) ")" ) "," (Set "(" (Set (Var "k")) ($#k4_pencil_4 :::"Pencils_of"::: ) (Set (Var "V")) ")" ) "#)" ))))); theorem :: PENCIL_4:17 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "V"))))) "holds" (Bool "not" (Bool (Set ($#k5_pencil_4 :::"PencilSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "k")) ")" ) "is" ($#v3_pencil_1 :::"void"::: ) ))))) ; theorem :: PENCIL_4:18 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "V")))) & (Bool (Num 3) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "V"))))) "holds" (Bool "not" (Bool (Set ($#k5_pencil_4 :::"PencilSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "k")) ")" ) "is" ($#v4_pencil_1 :::"degenerated"::: ) ))))) ; theorem :: PENCIL_4:19 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "V"))))) "holds" (Bool (Set ($#k5_pencil_4 :::"PencilSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "k")) ")" ) "is" ($#v5_pencil_1 :::"with_non_trivial_blocks"::: ) )))) ; theorem :: PENCIL_4:20 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "V"))))) "holds" (Bool (Set ($#k5_pencil_4 :::"PencilSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "k")) ")" ) "is" ($#v6_pencil_1 :::"identifying_close_blocks"::: ) )))) ; theorem :: PENCIL_4:21 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "V")))) & (Bool (Num 3) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "V"))))) "holds" (Bool (Set ($#k5_pencil_4 :::"PencilSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "k")) ")" ) "is" ($#l1_pre_topc :::"PLS":::))))) ; begin definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); let "m", "n" be ($#m1_hidden :::"Nat":::); func :::"SubspaceSet"::: "(" "V" "," "m" "," "n" ")" -> ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" "m" ($#k2_vectsp_9 :::"Subspaces_of"::: ) "V" ")" ) means :: PENCIL_4:def 6 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" "V" "st" (Bool "(" (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) "n") & (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set "m" ($#k2_vectsp_9 :::"Subspaces_of"::: ) (Set (Var "W")))) ")" )) ")" )); end; :: deftheorem defines :::"SubspaceSet"::: PENCIL_4:def 6 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" (Set (Var "m")) ($#k2_vectsp_9 :::"Subspaces_of"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k6_pencil_4 :::"SubspaceSet"::: ) "(" (Set (Var "V")) "," (Set (Var "m")) "," (Set (Var "n")) ")" )) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "b5"))) "iff" (Bool "ex" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k2_vectsp_9 :::"Subspaces_of"::: ) (Set (Var "W")))) ")" )) ")" )) ")" ))))); theorem :: PENCIL_4:22 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "V"))))) "holds" (Bool "not" (Bool (Set ($#k6_pencil_4 :::"SubspaceSet"::: ) "(" (Set (Var "V")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))))) ; theorem :: PENCIL_4:23 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "W1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "W2"))))) "holds" (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "m")) ($#k2_vectsp_9 :::"Subspaces_of"::: ) (Set (Var "W1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k2_vectsp_9 :::"Subspaces_of"::: ) (Set (Var "W2"))))))) ; theorem :: PENCIL_4:24 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "V")))) & (Bool (Set (Set (Var "m")) ($#k2_vectsp_9 :::"Subspaces_of"::: ) (Set (Var "V"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "m")) ($#k2_vectsp_9 :::"Subspaces_of"::: ) (Set (Var "W"))))) "holds" (Bool (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "W")))))))) ; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); let "m", "n" be ($#m1_hidden :::"Nat":::); func :::"GrassmannSpace"::: "(" "V" "," "m" "," "n" ")" -> ($#v1_pre_topc :::"strict"::: ) ($#l1_pre_topc :::"TopStruct"::: ) equals :: PENCIL_4:def 7 (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "(" "m" ($#k2_vectsp_9 :::"Subspaces_of"::: ) "V" ")" ) "," (Set "(" ($#k6_pencil_4 :::"SubspaceSet"::: ) "(" "V" "," "m" "," "n" ")" ")" ) "#)" ); end; :: deftheorem defines :::"GrassmannSpace"::: PENCIL_4:def 7 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k7_pencil_4 :::"GrassmannSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "(" (Set (Var "m")) ($#k2_vectsp_9 :::"Subspaces_of"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k6_pencil_4 :::"SubspaceSet"::: ) "(" (Set (Var "V")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) "#)" ))))); theorem :: PENCIL_4:25 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "V"))))) "holds" (Bool "not" (Bool (Set ($#k7_pencil_4 :::"GrassmannSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ) "is" ($#v3_pencil_1 :::"void"::: ) ))))) ; theorem :: PENCIL_4:26 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "V"))))) "holds" (Bool "not" (Bool (Set ($#k7_pencil_4 :::"GrassmannSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ) "is" ($#v4_pencil_1 :::"degenerated"::: ) ))))) ; theorem :: PENCIL_4:27 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "V"))))) "holds" (Bool (Set ($#k7_pencil_4 :::"GrassmannSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ) "is" ($#v5_pencil_1 :::"with_non_trivial_blocks"::: ) )))) ; theorem :: PENCIL_4:28 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "m")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "V"))))) "holds" (Bool (Set ($#k7_pencil_4 :::"GrassmannSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "m")) "," (Set "(" (Set (Var "m")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "is" ($#v6_pencil_1 :::"identifying_close_blocks"::: ) )))) ; theorem :: PENCIL_4:29 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Set (Var "m")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "V"))))) "holds" (Bool (Set ($#k7_pencil_4 :::"GrassmannSpace"::: ) "(" (Set (Var "V")) "," (Set (Var "m")) "," (Set "(" (Set (Var "m")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "is" ($#l1_pre_topc :::"PLS":::))))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"PairSet"::: "X" -> ($#m1_hidden :::"set"::: ) means :: PENCIL_4:def 8 (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )) ")" )) ")" )); end; :: deftheorem defines :::"PairSet"::: PENCIL_4:def 8 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k8_pencil_4 :::"PairSet"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )) ")" )) ")" )) ")" ))); registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k8_pencil_4 :::"PairSet"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "t", "X" be ($#m1_hidden :::"set"::: ) ; func :::"PairSet"::: "(" "t" "," "X" ")" -> ($#m1_hidden :::"set"::: ) means :: PENCIL_4:def 9 (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) "t" "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )) ")" )) ")" )); end; :: deftheorem defines :::"PairSet"::: PENCIL_4:def 9 : (Bool "for" (Set (Var "t")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k9_pencil_4 :::"PairSet"::: ) "(" (Set (Var "t")) "," (Set (Var "X")) ")" )) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "t")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )) ")" )) ")" )) ")" ))); registrationlet "t" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k9_pencil_4 :::"PairSet"::: ) "(" "t" "," "X" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "t" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k9_pencil_4 :::"PairSet"::: ) "(" "t" "," "X" ")" ) -> ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); func :::"PairSetFamily"::: "L" -> ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k8_pencil_4 :::"PairSet"::: ) "X" ")" ) means :: PENCIL_4:def 10 (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "l")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) "L") & (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k9_pencil_4 :::"PairSet"::: ) "(" (Set (Var "t")) "," (Set (Var "l")) ")" )) ")" ))) ")" )); end; :: deftheorem defines :::"PairSetFamily"::: PENCIL_4:def 10 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k8_pencil_4 :::"PairSet"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_pencil_4 :::"PairSetFamily"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "l")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set (Var "L"))) & (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k9_pencil_4 :::"PairSet"::: ) "(" (Set (Var "t")) "," (Set (Var "l")) ")" )) ")" ))) ")" )) ")" )))); registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); cluster (Set ($#k10_pencil_4 :::"PairSetFamily"::: ) "L") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "S" be ($#l1_pre_topc :::"TopStruct"::: ) ; func :::"VeroneseSpace"::: "S" -> ($#v1_pre_topc :::"strict"::: ) ($#l1_pre_topc :::"TopStruct"::: ) equals :: PENCIL_4:def 11 (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "(" ($#k8_pencil_4 :::"PairSet"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ")" ) "," (Set "(" ($#k10_pencil_4 :::"PairSetFamily"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "S") ")" ) "#)" ); end; :: deftheorem defines :::"VeroneseSpace"::: PENCIL_4:def 11 : (Bool "for" (Set (Var "S")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool (Set ($#k11_pencil_4 :::"VeroneseSpace"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "(" ($#k8_pencil_4 :::"PairSet"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ")" ) "," (Set "(" ($#k10_pencil_4 :::"PairSetFamily"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S"))) ")" ) "#)" ))); registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; cluster (Set ($#k11_pencil_4 :::"VeroneseSpace"::: ) "S") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; cluster (Set ($#k11_pencil_4 :::"VeroneseSpace"::: ) "S") -> ($#v1_pre_topc :::"strict"::: ) ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#~v4_pencil_1 "non" ($#v4_pencil_1 :::"degenerated"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; cluster (Set ($#k11_pencil_4 :::"VeroneseSpace"::: ) "S") -> ($#v1_pre_topc :::"strict"::: ) ($#~v4_pencil_1 "non" ($#v4_pencil_1 :::"degenerated"::: ) ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_pencil_1 "non" ($#v3_pencil_1 :::"void"::: ) ) ($#v5_pencil_1 :::"with_non_trivial_blocks"::: ) ($#l1_pre_topc :::"TopStruct"::: ) ; cluster (Set ($#k11_pencil_4 :::"VeroneseSpace"::: ) "S") -> ($#v1_pre_topc :::"strict"::: ) ($#v5_pencil_1 :::"with_non_trivial_blocks"::: ) ; end; registrationlet "S" be ($#v6_pencil_1 :::"identifying_close_blocks"::: ) ($#l1_pre_topc :::"TopStruct"::: ) ; cluster (Set ($#k11_pencil_4 :::"VeroneseSpace"::: ) "S") -> ($#v1_pre_topc :::"strict"::: ) ($#v6_pencil_1 :::"identifying_close_blocks"::: ) ; end;