:: The Friendship Theorem :: by Karol P\kak :: :: Received May 15, 2012 :: Copyright (c) 2012-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 RELAT_1, TARSKI, XBOOLE_0, ZFMISC_1, RELAT_2, FUNCT_1, SUBSET_1, FINSET_1, NUMBERS, NAT_1, INT_1, ARYTM_3, CARD_1, XXREAL_0, ARYTM_1, INT_2, CARD_2, FINSEQ_1, ORDINAL4, FINSEQ_2, XCMPLX_0, NEWTON, RFINSEQ, FRIENDS1; notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, RELAT_2, ENUMSET1, FUNCT_1, ORDINAL1, SUBSET_1, RELSET_1, FUNCT_2, FINSET_1, CARD_1, CARD_2, NUMBERS, XCMPLX_0, XXREAL_0, INT_1, INT_2, FINSEQ_1, FINSEQ_2, NEWTON, RFINSEQ, NAT_D; constructors RELAT_2, DOMAIN_1, RELSET_1, NAT_1, REAL_1, CARD_2, WELLORD2, FINSEQ_2, NEWTON, RFINSEQ, NAT_D; registrations RELAT_1, FINSEQ_2, XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, CARD_1, FINSEQ_1, NEWTON; requirements SUBSET, BOOLE, NUMERALS, REAL, ARITHM; begin :: Preliminaries reserve x,y,z for object, X for set, i,k,n,m for Nat, R for Relation, P for finite Relation, p,q for FinSequence; registration let P; let x be object; cluster Im(P,x) -> finite; end; theorem :: FRIENDS1:1 card R = card (R~); theorem :: FRIENDS1:2 R is symmetric implies R.:X = R"X; theorem :: FRIENDS1:3 (p /^k)^(p|k) = (q /^n)^(q|n) & k <= n & n <= len p implies p = (q /^(n-'k)) ^ (q| (n-'k)); theorem :: FRIENDS1:4 n in dom q & p = (q /^n)^(q|n) implies q = (p/^(len p-'n))^p| (len p-'n); theorem :: FRIENDS1:5 (p /^k)^(p|k) = (q /^n)^(q|n) implies ex i st p = (q /^i) ^ (q|i); scheme :: FRIENDS1:sch 1 Sch{X()->non empty set,n() -> non zero Nat, P[set]}: ex C be Cardinal st n()*`C = card {F where F is Element of n()-tuples_on X():P[F]} provided for p,q be FinSequence of X() st p^q is n() -element & P[p^q] holds P[q^p] and for p be Element of n()-tuples_on X() st P[p] for i be Nat st i < n() & p = (p/^i)^(p|i) holds i = 0; theorem :: FRIENDS1:6 for X be non empty set, A be non empty finite Subset of X for P be Function of X,bool X st for x st x in X holds card (P.x)=n holds card {F where F is Element of (k+1)-tuples_on X: F.1 in A & for i st i in Seg k holds F.(i+1) in P.(F.i)} = card A * (n |^ k); theorem :: FRIENDS1:7 len p is prime & (ex i st 0 < i & i < len p & p = (p/^i) ^ (p|i)) implies rng p c= {p.1}; begin :: The Friendship Graph definition let R; let x be Element of field R; attr x is universal_friend means :: FRIENDS1:def 1 for y st y in field R\{x} holds [x,y] in R; end; definition let R be Relation; attr R is with_universal_friend means :: FRIENDS1:def 2 ex x be Element of field R st x is universal_friend; end; notation let R be Relation; antonym R is without_universal_friend for R is with_universal_friend; end; definition let R be Relation; attr R is friendship_graph_like means :: FRIENDS1:def 3 for x,y being object st x in field R & y in field R & x <> y ex z being object st Im(R,x) /\ Coim(R,y) ={z}; end; registration cluster finite symmetric irreflexive friendship_graph_like for Relation; end; ::$N Friendship graph definition mode Friendship_Graph is finite symmetric irreflexive friendship_graph_like Relation; end; reserve FSG for Friendship_Graph; theorem :: FRIENDS1:8 2 divides card Im(FSG,x); theorem :: FRIENDS1:9 x in field FSG & y in field FSG & not [x,y] in FSG implies card Im(FSG,x) = card Im(FSG,y); theorem :: FRIENDS1:10 FSG is without_universal_friend & x in field FSG implies card Im(FSG,x) > 2; theorem :: FRIENDS1:11 FSG is without_universal_friend & x in field FSG & y in field FSG implies card Im(FSG,x) = card Im(FSG,y); theorem :: FRIENDS1:12 FSG is without_universal_friend & x in field FSG implies card field FSG = 1 + card Im(FSG,x) * (card Im(FSG,x)-1); theorem :: FRIENDS1:13 for x,y be Element of field FSG st x is universal_friend & x <> y holds ex z being object st Im(FSG,y) = {x,z} & Im(FSG,z) = {x,y}; begin :: The Friendship Theorem ::$N Friendship theorem theorem :: FRIENDS1:14 FSG is non empty implies FSG is with_universal_friend;