:: The Collinearity Structure
:: by Wojciech Skaba
::
:: Received May 9, 1990
:: Copyright (c) 1990-2021 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;