Volume 3, 1991

University of Bialystok

Copyright (c) 1991 Association of Mizar Users

### The abstract of the Mizar article:

### Shear Theorems and Their Role in Affine Geometry

**by****Jolanta Swierzynska, and****Bogdan Swierzynski**- Received April 19, 1991
- MML identifier: CONMETR1

- [ Mizar article, MML identifier index ]

environ vocabulary DIRAF, ANALOAF, AFF_1, AFF_2, ANALMETR, CONMETR, CONAFFM, CONMETR1; notation SUBSET_1, STRUCT_0, ANALOAF, DIRAF, AFF_1, ANALMETR, AFF_2, CONAFFM, CONMETR; constructors AFF_1, AFF_2, CONAFFM, CONMETR, XBOOLE_0; clusters ANALMETR, ZFMISC_1, XBOOLE_0; requirements SUBSET; begin reserve X for AffinPlane; reserve o,a,a1,a2,a3,a4,b,b1,b2,b3,b4,c,c1,c2,d,d1,d2, d3,d4,d5,e1,e2,x,y,z for Element of X; reserve Y,Z,M,N,A,K,C for Subset of X; definition let X; attr X is satisfying_minor_Scherungssatz means :: CONMETR1:def 1 for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M // N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4; synonym X satisfies_minor_SCH; end; definition let X; attr X is satisfying_major_Scherungssatz means :: CONMETR1:def 2 for o,a1,a2,a3,a4,b1,b2,b3,b4,M,N st M is_line & N is_line & o in M & o in N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4; synonym X satisfies_major_SCH; end; definition let X; attr X is satisfying_Scherungssatz means :: CONMETR1:def 3 for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M is_line & N is_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4; synonym X satisfies_SCH; end; definition let X; attr X is satisfying_indirect_Scherungssatz means :: CONMETR1:def 4 for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M is_line & N is_line & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4; synonym X satisfies_SCH*; end; definition let X; attr X is satisfying_minor_indirect_Scherungssatz means :: CONMETR1:def 5 for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M // N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4; synonym X satisfies_minor_SCH*; end; definition let X; attr X is satisfying_major_indirect_Scherungssatz means :: CONMETR1:def 6 for o,a1,a2,a3,a4,b1,b2,b3,b4,M,N st M is_line & N is_line & o in M & o in N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4; synonym X satisfies_major_SCH*; end; theorem :: CONMETR1:1 X satisfies_SCH* iff (X satisfies_minor_SCH* & X satisfies_major_SCH*); theorem :: CONMETR1:2 X satisfies_SCH iff (X satisfies_minor_SCH & X satisfies_major_SCH); theorem :: CONMETR1:3 X satisfies_minor_SCH* implies X satisfies_minor_SCH; theorem :: CONMETR1:4 X satisfies_major_SCH* implies X satisfies_major_SCH; theorem :: CONMETR1:5 X satisfies_SCH* implies X satisfies_SCH; theorem :: CONMETR1:6 X satisfies_des implies X satisfies_minor_SCH; theorem :: CONMETR1:7 X satisfies_DES implies X satisfies_major_SCH; theorem :: CONMETR1:8 X satisfies_DES iff X satisfies_SCH; theorem :: CONMETR1:9 X satisfies_pap iff X satisfies_minor_SCH*; theorem :: CONMETR1:10 X satisfies_PAP iff X satisfies_major_SCH*; theorem :: CONMETR1:11 X satisfies_PPAP iff X satisfies_SCH*; theorem :: CONMETR1:12 X satisfies_major_SCH* implies X satisfies_minor_SCH*; reserve X for OrtAfPl; reserve o',a',a1',a2',a3',a4',b',b1',b2',b3',b4',c',c1' for Element of X; reserve o,a,a1,a2,a3,a4,b,b1,b2,b3,b4,c,c1 for Element of Af(X); reserve M',N' for Subset of X; reserve A,M,N for Subset of Af(X); theorem :: CONMETR1:13 Af(X) satisfies_SCH iff SCH_holds_in X; theorem :: CONMETR1:14 TDES_holds_in X iff Af(X) satisfies_TDES; theorem :: CONMETR1:15 Af(X) satisfies_des iff des_holds_in X; theorem :: CONMETR1:16 PAP_holds_in X iff Af(X) satisfies_PAP; theorem :: CONMETR1:17 DES_holds_in X iff Af(X) satisfies_DES;

Back to top