:: The Collinearity Structure :: by Wojciech Skaba :: :: Received May 9, 1990 :: Copyright (c) 1990-2016 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, RELAT_2, INCSP_1, NUMBERS, COLLSP, PENCIL_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, DOMAIN_1, STRUCT_0, PRE_TOPC; constructors DOMAIN_1, NUMBERS, STRUCT_0; registrations XBOOLE_0, ORDINAL1, STRUCT_0; requirements NUMERALS, SUBSET, BOOLE; begin :: AUXILIARY THEOREMS reserve X for set; definition let X; mode Relation3 of X -> set means :: COLLSP:def 1 it c= [:X,X,X:]; end; theorem :: COLLSP:1 X = {} or ex a be set st {a} = X or ex a,b be set st a<>b & a in X & b in X; :: ********************* :: * COLLINEARITY * :: ********************* definition struct(1-sorted) CollStr (# carrier -> set, Collinearity -> Relation3 of the carrier #); end; registration cluster non empty strict for CollStr; end; reserve CS for non empty CollStr; reserve a,b,c for Point of CS; definition let CS, a,b,c; pred a,b,c are_collinear means :: COLLSP:def 2 [a,b,c] in the Collinearity of CS; end; definition let IT be non empty CollStr; attr IT is reflexive means :: COLLSP:def 3 for a,b,c being Point of IT st a=b or a=c or b=c holds [a,b,c] in the Collinearity of IT; end; definition let IT be non empty CollStr; attr IT is transitive means :: COLLSP:def 4 for a,b,p,q,r being Point of IT st a<>b & [a,b,p] in the Collinearity of IT & [a,b,q] in the Collinearity of IT & [a,b,r] in the Collinearity of IT holds [p,q,r] in the Collinearity of IT; end; registration cluster strict reflexive transitive for non empty CollStr; end; definition mode CollSp is reflexive transitive non empty CollStr; end; reserve CLSP for CollSp; reserve a,b,c,d,p,q,r for Point of CLSP; theorem :: COLLSP:2 (a=b or a=c or b=c) implies a,b,c are_collinear; theorem :: COLLSP:3 a<>b & a,b,p are_collinear & a,b,q are_collinear & a,b,r are_collinear implies p,q,r are_collinear; theorem :: COLLSP:4 a,b,c are_collinear implies b,a,c are_collinear & a,c,b are_collinear; theorem :: COLLSP:5 a,b,a are_collinear; theorem :: COLLSP:6 a<>b & a,b,c are_collinear & a,b,d are_collinear implies a,c,d are_collinear; theorem :: COLLSP:7 a,b,c are_collinear implies b,a,c are_collinear; theorem :: COLLSP:8 a,b,c are_collinear implies b,c,a are_collinear; theorem :: COLLSP:9 p<>q & a,b,p are_collinear & a,b,q are_collinear & p,q,r are_collinear implies a,b,r are_collinear; :: ******************* :: * LINES * :: ******************* definition let CLSP,a,b; func Line(a,b) -> set equals :: COLLSP:def 5 {p: a,b,p are_collinear}; end; theorem :: COLLSP:10 a in Line(a,b) & b in Line(a,b); theorem :: COLLSP:11 a,b,r are_collinear iff r in Line(a,b); :: ************************************ :: * PROPER COLLINEARITY SPACES * :: ************************************ reserve i,j,k for Element of NAT; definition let IT be non empty CollStr; attr IT is proper means :: COLLSP:def 6 ex a,b,c being Point of IT st not a,b,c are_collinear; end; registration cluster strict proper for CollSp; end; reserve CLSP for proper CollSp; reserve a,b,c,p,q,r for Point of CLSP; theorem :: COLLSP:12 for p,q holds p<>q implies ex r st not p,q,r are_collinear; definition let CLSP; mode LINE of CLSP -> set means :: COLLSP:def 7 ex a,b st a<>b & it=Line(a,b); end; reserve P,Q for LINE of CLSP; theorem :: COLLSP:13 a=b implies Line(a,b) = the carrier of CLSP; theorem :: COLLSP:14 for P ex a,b st a<>b & a in P & b in P; theorem :: COLLSP:15 a <> b implies ex P st a in P & b in P; theorem :: COLLSP:16 p in P & q in P & r in P implies p,q,r are_collinear; theorem :: COLLSP:17 P c= Q implies P = Q; theorem :: COLLSP:18 p<>q & p in P & q in P implies Line(p,q) c= P; theorem :: COLLSP:19 p<>q & p in P & q in P implies Line(p,q) = P; theorem :: COLLSP:20 p<>q & p in P & q in P & p in Q & q in Q implies P = Q; theorem :: COLLSP:21 P = Q or P misses Q or ex p st P /\ Q = {p}; theorem :: COLLSP:22 a<>b implies Line(a,b) <> the carrier of CLSP;