:: JORDAN_A semantic presentation begin theorem :: JORDAN_A:1 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#v1_pscomp_1 :::"continuous"::: ) ($#m1_subset_1 :::"RealMap":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) "is" ($#v1_rcomp_1 :::"compact"::: ) )))) ; theorem :: JORDAN_A:2 (Bool "for" (Set (Var "A")) "being" ($#v1_rcomp_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "B"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))) ; theorem :: JORDAN_A:3 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#v1_pscomp_1 :::"continuous"::: ) ($#m1_subset_1 :::"RealMap":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) "}" ) & (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "G")))) ")" )) ")" )) "holds" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set ($#k3_borsuk_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k3_borsuk_1 :::":]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" (Set (Var "g")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")) ")" ))))))) ; theorem :: JORDAN_A:4 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#v1_pscomp_1 :::"continuous"::: ) ($#m1_subset_1 :::"RealMap":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "}" ) & (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "G")))) ")" )) ")" )) "holds" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set ($#k3_borsuk_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k3_borsuk_1 :::":]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" (Set (Var "g")) ($#k7_relset_1 :::".:"::: ) (Set (Var "B")) ")" ))))))) ; theorem :: JORDAN_A:5 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "C")))) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C"))))) "holds" (Bool ($#r1_jordan6 :::"LE"::: ) (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C"))) "," (Set (Var "q")) "," (Set (Var "C"))))) ; theorem :: JORDAN_A:6 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "C"))))) "holds" (Bool ($#r1_jordan6 :::"LE"::: ) (Set (Var "q")) "," (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C"))) "," (Set (Var "C"))))) ; begin definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Eucl_dist"::: "n" -> ($#m1_subset_1 :::"RealMap":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) ($#k2_borsuk_1 :::":]"::: ) ) means :: JORDAN_A:def 1 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) ))); end; :: deftheorem defines :::"Eucl_dist"::: JORDAN_A:def 1 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan_a :::"Eucl_dist"::: ) (Set (Var "n")))) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set (Var "b2")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) ))) ")" ))); definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "f" be ($#m1_subset_1 :::"RealMap":::) "of" (Set (Const "T")); redefine attr "f" is :::"continuous"::: means :: JORDAN_A:def 2 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" "T" (Bool "for" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set "f" ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) (Bool "ex" (Set (Var "V")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "p")) "st" (Bool (Set "f" ($#k7_relset_1 :::".:"::: ) (Set (Var "V"))) ($#r1_tarski :::"c="::: ) (Set (Var "N")))))); end; :: deftheorem defines :::"continuous"::: JORDAN_A:def 2 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"RealMap":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_pscomp_1 :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "N")) "being" ($#m1_rcomp_1 :::"Neighbourhood"::: ) "of" (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) (Bool "ex" (Set (Var "V")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "p")) "st" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "V"))) ($#r1_tarski :::"c="::: ) (Set (Var "N")))))) ")" ))); registrationlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k1_jordan_a :::"Eucl_dist"::: ) "n") -> ($#v1_pscomp_1 :::"continuous"::: ) ; end; begin theorem :: JORDAN_A:7 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_subset_1 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k4_jordan1k :::"dist_min"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; begin theorem :: JORDAN_A:8 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r1_jordan6 :::"LE"::: ) (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "C"))) & (Bool ($#r1_jordan6 :::"LE"::: ) (Set (Var "q")) "," (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C"))) "," (Set (Var "C"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q")))) "holds" (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_jordan6 :::"Segment"::: ) "(" (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C")) ")" ) "," (Set (Var "p")) "," (Set (Var "q")) ")" )))) ; theorem :: JORDAN_A:9 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r1_jordan6 :::"LE"::: ) (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C"))) "," (Set (Var "q")) "," (Set (Var "C")))) "holds" (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C")) ")" ) "," (Set (Var "q")) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_jordan6 :::"Segment"::: ) "(" (Set "(" ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C")) ")" ) "," (Set (Var "q")) ")" )))) ; theorem :: JORDAN_A:10 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r1_jordan6 :::"LE"::: ) (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C"))) "," (Set (Var "q")) "," (Set (Var "C")))) "holds" (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "q")) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")) ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_jordan6 :::"Segment"::: ) "(" (Set "(" ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")) ")" ) "," (Set (Var "q")) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")) ")" ) ")" )))) ; theorem :: JORDAN_A:11 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r1_jordan6 :::"LE"::: ) (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "C"))) & (Bool ($#r1_jordan6 :::"LE"::: ) (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C"))) "," (Set (Var "p")) "," (Set (Var "C")))) "holds" (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_jordan6 :::"Segment"::: ) "(" (Set "(" ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")) ")" ) "," (Set (Var "p")) "," (Set (Var "q")) ")" )))) ; theorem :: JORDAN_A:12 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r1_jordan6 :::"LE"::: ) (Set (Var "p")) "," (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C"))) "," (Set (Var "C"))) & (Bool ($#r1_jordan6 :::"LE"::: ) (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C"))) "," (Set (Var "q")) "," (Set (Var "C")))) "holds" (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_jordan6 :::"R_Segment"::: ) "(" (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C")) ")" ) "," (Set (Var "p")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_jordan6 :::"L_Segment"::: ) "(" (Set "(" ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")) ")" ) "," (Set (Var "q")) ")" ")" ))))) ; theorem :: JORDAN_A:13 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r1_jordan6 :::"LE"::: ) (Set (Var "p")) "," (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C"))) "," (Set (Var "C")))) "holds" (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")) ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_jordan6 :::"R_Segment"::: ) "(" (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C")) ")" ) "," (Set (Var "p")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_jordan6 :::"L_Segment"::: ) "(" (Set "(" ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")) ")" ) ")" ")" ))))) ; theorem :: JORDAN_A:14 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k4_jordan6 :::"R_Segment"::: ) "(" (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C")) ")" ) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_jordan6 :::"Segment"::: ) "(" (Set "(" ($#k8_jordan6 :::"Upper_Arc"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C")) ")" ) "," (Set (Var "p")) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C")) ")" ) ")" )))) ; theorem :: JORDAN_A:15 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k3_jordan6 :::"L_Segment"::: ) "(" (Set "(" ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")) ")" ) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_jordan6 :::"Segment"::: ) "(" (Set "(" ($#k9_jordan6 :::"Lower_Arc"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C")) ")" ) "," (Set (Var "p")) ")" )))) ; theorem :: JORDAN_A:16 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C"))))) "holds" (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")) ")" ) "," (Set (Var "C")) ")" ) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p")) "," (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")))))) ; theorem :: JORDAN_A:17 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool ($#r1_jordan6 :::"LE"::: ) (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "C")))) "holds" (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "C")) ")" ) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p")) "," (Set (Var "q"))))) ; theorem :: JORDAN_A:18 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) "holds" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")) ")" ) "," (Set (Var "C")) ")" ))) ; theorem :: JORDAN_A:19 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "q")) "," (Set "(" ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")) ")" ) "," (Set (Var "C")) ")" ) "is" ($#v2_compts_1 :::"compact"::: ) ))) ; theorem :: JORDAN_A:20 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool ($#r1_jordan6 :::"LE"::: ) (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "C")))) "holds" (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "C")) ")" ) "is" ($#v2_compts_1 :::"compact"::: ) ))) ; begin definitionlet "C" be ($#m1_subset_1 :::"Simple_closed_curve":::); mode :::"Segmentation"::: "of" "C" -> ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) means :: JORDAN_A:def 3 (Bool "(" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) "C")) & (Bool it "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Num 8) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) it)) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) it) ($#r1_tarski :::"c="::: ) "C") & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) it))) "holds" (Bool ($#r1_jordan6 :::"LE"::: ) (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) "," (Set it ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) "," "C") ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) it))) "holds" (Bool (Set (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" it ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set "(" it ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," "C" ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" it ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" it ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) "," "C" ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" it ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_tarski :::"}"::: ) )) ")" ) & (Bool (Set (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" it ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) it ")" ) ")" ) "," (Set "(" it ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," "C" ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" it ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set "(" it ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) "," "C" ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" it ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" it ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) it ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) "," (Set "(" it ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) it ")" ) ")" ) "," "C" ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" it ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) it ")" ) ")" ) "," (Set "(" it ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," "C" ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" it ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) it ")" ) ")" ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" it ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) it ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) "," (Set "(" it ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) it ")" ) ")" ) "," "C" ")" ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" it ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set "(" it ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) "," "C" ")" )) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) it)) & (Bool (Bool "not" (Set (Var "i")) "," (Set (Var "j")) ($#r1_gobrd10 :::"are_adjacent1"::: ) ))) "holds" (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" it ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set "(" it ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," "C" ")" ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" it ($#k7_partfun1 :::"/."::: ) (Set (Var "j")) ")" ) "," (Set "(" it ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," "C" ")" )) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) it))) "holds" (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" it ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) it ")" ) ")" ) "," (Set "(" it ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," "C" ")" ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" it ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set "(" it ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," "C" ")" )) ")" ) ")" ); end; :: deftheorem defines :::"Segmentation"::: JORDAN_A:def 3 : (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Var "C"))) "iff" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C")))) & (Bool (Set (Var "b2")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Num 8) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))))) "holds" (Bool ($#r1_jordan6 :::"LE"::: ) (Set (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) "," (Set (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) "," (Set (Var "C"))) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "C")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) "," (Set (Var "C")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_tarski :::"}"::: ) )) ")" ) & (Bool (Set (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2")) ")" ) ")" ) "," (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set (Var "C")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) "," (Set (Var "C")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2")) ")" ) ")" ) "," (Set (Var "C")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2")) ")" ) ")" ) "," (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set (Var "C")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2")) ")" ) ")" ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2")) ")" ) ")" ) "," (Set (Var "C")) ")" ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) "," (Set (Var "C")) ")" )) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2")))) & (Bool (Bool "not" (Set (Var "i")) "," (Set (Var "j")) ($#r1_gobrd10 :::"are_adjacent1"::: ) ))) "holds" (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "C")) ")" ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j")) ")" ) "," (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "C")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))))) "holds" (Bool (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2")) ")" ) ")" ) "," (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set (Var "C")) ")" ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "C")) ")" )) ")" ) ")" ) ")" ))); registrationlet "C" be ($#m1_subset_1 :::"Simple_closed_curve":::); cluster -> ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) for ($#m1_jordan_a :::"Segmentation"::: ) "of" "C"; end; theorem :: JORDAN_A:21 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "S")) "being" ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Set (Var "S")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Var "C")))))) ; begin definitionlet "C" be ($#m1_subset_1 :::"Simple_closed_curve":::); let "i" be ($#m1_hidden :::"Nat":::); let "S" be ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Const "C")); func :::"Segm"::: "(" "S" "," "i" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) equals :: JORDAN_A:def 4 (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" "S" ($#k7_partfun1 :::"/."::: ) "i" ")" ) "," (Set "(" "S" ($#k7_partfun1 :::"/."::: ) (Set "(" "i" ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," "C" ")" ) if (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) "i") & (Bool "i" ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "S")) ")" ) otherwise (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" "S" ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "S" ")" ) ")" ) "," (Set "(" "S" ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," "C" ")" ); end; :: deftheorem defines :::"Segm"::: JORDAN_A:def 4 : (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Var "C")) "holds" (Bool "(" "(" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "S"))))) "implies" (Bool (Set ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "S")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "S")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set (Var "C")) ")" )) ")" & "(" (Bool (Bool "(" "not" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) "or" "not" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "S")))) ")" )) "implies" (Bool (Set ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_jordan7 :::"Segment"::: ) "(" (Set "(" (Set (Var "S")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "S")) ")" ) ")" ) "," (Set "(" (Set (Var "S")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set (Var "C")) ")" )) ")" ")" )))); theorem :: JORDAN_A:22 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "S"))))) "holds" (Bool (Set ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set (Var "i")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "C")))))) ; registrationlet "C" be ($#m1_subset_1 :::"Simple_closed_curve":::); let "S" be ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Const "C")); let "i" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k2_jordan_a :::"Segm"::: ) "(" "S" "," "i" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ; end; theorem :: JORDAN_A:23 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "S")) "being" ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "S")))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set (Var "i")) ")" )) ")" ))))) ; theorem :: JORDAN_A:24 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "S")) "being" ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "S")))) & (Bool (Bool "not" (Set (Var "i")) "," (Set (Var "j")) ($#r1_gobrd10 :::"are_adjacent1"::: ) ))) "holds" (Bool (Set ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set (Var "i")) ")" ) ($#r1_subset_1 :::"misses"::: ) (Set ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set (Var "j")) ")" ))))) ; theorem :: JORDAN_A:25 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "S")) "being" ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "S")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1)))) "holds" (Bool (Set ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "S")) ")" ) ")" ) ($#r1_subset_1 :::"misses"::: ) (Set ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set (Var "j")) ")" ))))) ; theorem :: JORDAN_A:26 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "S")) "being" ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "S")))) & (Bool (Set (Var "i")) "," (Set (Var "j")) ($#r1_gobrd10 :::"are_adjacent1"::: ) )) "holds" (Bool (Set (Set "(" ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set (Var "i")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set (Var "j")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "S")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: JORDAN_A:27 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "S")) "being" ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "S")))) & (Bool (Set (Var "i")) "," (Set (Var "j")) ($#r1_gobrd10 :::"are_adjacent1"::: ) )) "holds" (Bool (Set ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set (Var "i")) ")" ) ($#r2_subset_1 :::"meets"::: ) (Set ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set (Var "j")) ")" ))))) ; theorem :: JORDAN_A:28 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "S")) "being" ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "S")) ")" ) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Num 1) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "S")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: JORDAN_A:29 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "S")) "being" ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Var "C")) "holds" (Bool (Set ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "S")) ")" ) ")" ) ($#r2_subset_1 :::"meets"::: ) (Set ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Num 1) ")" )))) ; theorem :: JORDAN_A:30 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "S")) "being" ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "S")) ")" ) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "S")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "S")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "S")) ")" ) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: JORDAN_A:31 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "S")) "being" ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Var "C")) "holds" (Bool (Set ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "S")) ")" ) ")" ) ($#r2_subset_1 :::"meets"::: ) (Set ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "S")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )))) ; begin definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "C" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); func :::"diameter"::: "C" -> ($#m1_subset_1 :::"Real":::) means :: JORDAN_A:def 5 (Bool "ex" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) "n" ")" ) "st" (Bool "(" (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) "C") & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_tbsp_1 :::"diameter"::: ) (Set (Var "W")))) ")" )); end; :: deftheorem defines :::"diameter"::: JORDAN_A:def 5 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_jordan_a :::"diameter"::: ) (Set (Var "C")))) "iff" (Bool "ex" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set (Var "C"))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_tbsp_1 :::"diameter"::: ) (Set (Var "W")))) ")" )) ")" )))); definitionlet "C" be ($#m1_subset_1 :::"Simple_closed_curve":::); let "S" be ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Const "C")); func :::"diameter"::: "S" -> ($#m1_subset_1 :::"Real":::) means :: JORDAN_A:def 6 (Bool "ex" (Set (Var "S1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "S1")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k3_jordan_a :::"diameter"::: ) (Set "(" ($#k2_jordan_a :::"Segm"::: ) "(" "S" "," (Set (Var "i")) ")" ")" ) ")" ) where i "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "S")) "}" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_2 :::"max"::: ) (Set (Var "S1")))) ")" )); end; :: deftheorem defines :::"diameter"::: JORDAN_A:def 6 : (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "S")) "being" ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_jordan_a :::"diameter"::: ) (Set (Var "S")))) "iff" (Bool "ex" (Set (Var "S1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "S1")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k3_jordan_a :::"diameter"::: ) (Set "(" ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set (Var "i")) ")" ")" ) ")" ) where i "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "S")))) "}" ) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_2 :::"max"::: ) (Set (Var "S1")))) ")" )) ")" )))); theorem :: JORDAN_A:32 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "S")) "being" ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_jordan_a :::"diameter"::: ) (Set "(" ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_jordan_a :::"diameter"::: ) (Set (Var "S"))))))) ; theorem :: JORDAN_A:33 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "S")) "being" ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_jordan_a :::"diameter"::: ) (Set "(" ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set (Var "i")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))) ")" )) "holds" (Bool (Set ($#k4_jordan_a :::"diameter"::: ) (Set (Var "S"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e")))))) ; theorem :: JORDAN_A:34 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "e")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "S")) "being" ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Var "C")) "st" (Bool (Set ($#k4_jordan_a :::"diameter"::: ) (Set (Var "S"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e")))))) ; begin definitionlet "C" be ($#m1_subset_1 :::"Simple_closed_curve":::); let "S" be ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Const "C")); func :::"S-Gap"::: "S" -> ($#m1_subset_1 :::"Real":::) means :: JORDAN_A:def 7 (Bool "ex" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "S1")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k4_jordan1k :::"dist_min"::: ) "(" (Set "(" ($#k2_jordan_a :::"Segm"::: ) "(" "S" "," (Set (Var "i")) ")" ")" ) "," (Set "(" ($#k2_jordan_a :::"Segm"::: ) "(" "S" "," (Set (Var "j")) ")" ")" ) ")" ")" ) where i, j "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "S")) & (Bool (Bool "not" (Set (Var "i")) "," (Set (Var "j")) ($#r1_gobrd10 :::"are_adjacent1"::: ) )) ")" ) "}" ) & (Bool (Set (Var "S2")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k4_jordan1k :::"dist_min"::: ) "(" (Set "(" ($#k2_jordan_a :::"Segm"::: ) "(" "S" "," (Set "(" ($#k3_finseq_1 :::"len"::: ) "S" ")" ) ")" ")" ) "," (Set "(" ($#k2_jordan_a :::"Segm"::: ) "(" "S" "," (Set (Var "k")) ")" ")" ) ")" ")" ) where k "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) "S" ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1))) ")" ) "}" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_xxreal_0 :::"min"::: ) "(" (Set "(" ($#k2_xxreal_2 :::"min"::: ) (Set (Var "S1")) ")" ) "," (Set "(" ($#k2_xxreal_2 :::"min"::: ) (Set (Var "S2")) ")" ) ")" )) ")" )); end; :: deftheorem defines :::"S-Gap"::: JORDAN_A:def 7 : (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "S")) "being" ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_jordan_a :::"S-Gap"::: ) (Set (Var "S")))) "iff" (Bool "ex" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "S1")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k4_jordan1k :::"dist_min"::: ) "(" (Set "(" ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set (Var "i")) ")" ")" ) "," (Set "(" ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set (Var "j")) ")" ")" ) ")" ")" ) where i, j "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "S")))) & (Bool (Bool "not" (Set (Var "i")) "," (Set (Var "j")) ($#r1_gobrd10 :::"are_adjacent1"::: ) )) ")" ) "}" ) & (Bool (Set (Var "S2")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k4_jordan1k :::"dist_min"::: ) "(" (Set "(" ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "S")) ")" ) ")" ")" ) "," (Set "(" ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set (Var "k")) ")" ")" ) ")" ")" ) where k "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "S")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1))) ")" ) "}" ) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_xxreal_0 :::"min"::: ) "(" (Set "(" ($#k2_xxreal_2 :::"min"::: ) (Set (Var "S1")) ")" ) "," (Set "(" ($#k2_xxreal_2 :::"min"::: ) (Set (Var "S2")) ")" ) ")" )) ")" )) ")" )))); theorem :: JORDAN_A:35 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "S")) "being" ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Var "C")) (Bool "ex" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k4_jordan1k :::"dist_min"::: ) "(" (Set "(" ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set (Var "i")) ")" ")" ) "," (Set "(" ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set (Var "j")) ")" ")" ) ")" ")" ) where i, j "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "S")))) & (Bool (Set ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set (Var "i")) ")" ) ($#r1_subset_1 :::"misses"::: ) (Set ($#k2_jordan_a :::"Segm"::: ) "(" (Set (Var "S")) "," (Set (Var "j")) ")" )) ")" ) "}" ) & (Bool (Set ($#k5_jordan_a :::"S-Gap"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k2_xxreal_2 :::"min"::: ) (Set (Var "F")))) ")" )))) ; theorem :: JORDAN_A:36 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Simple_closed_curve":::) (Bool "for" (Set (Var "S")) "being" ($#m1_jordan_a :::"Segmentation"::: ) "of" (Set (Var "C")) "holds" (Bool (Set ($#k5_jordan_a :::"S-Gap"::: ) (Set (Var "S"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )))) ;