:: The Friendship Theorem
:: by Karol P\kak
::
:: Received May 15, 2012
:: Copyright (c) 2012-2021 Association of Mizar Users


registration
let P be finite Relation;
let x be object ;
cluster Im (P,x) -> finite ;
coherence
Im (P,x) is finite
proof end;
end;

Lm1: for k, n being Nat holds
( n * k = n *` k & n + k = n +` k )

proof end;

theorem Th1: :: FRIENDS1:1
for R being Relation holds card R = card (R ~)
proof end;

Lm2: for x being object
for R being Relation st R is irreflexive holds
not [x,x] in R

proof end;

Lm3: for x, y being object
for R being Relation st R is symmetric & [x,y] in R holds
[y,x] in R

proof end;

theorem Th2: :: FRIENDS1:2
for X being set
for R being Relation st R is symmetric holds
R .: X = R " X
proof end;

Lm4: for k being Nat
for p being FinSequence st not k in dom p holds
(p /^ k) ^ (p | k) = p

proof end;

theorem Th3: :: FRIENDS1:3
for k, n being Nat
for p, q being FinSequence st (p /^ k) ^ (p | k) = (q /^ n) ^ (q | n) & k <= n & n <= len p holds
p = (q /^ (n -' k)) ^ (q | (n -' k))
proof end;

theorem Th4: :: FRIENDS1:4
for n being Nat
for p, q being FinSequence st n in dom q & p = (q /^ n) ^ (q | n) holds
q = (p /^ ((len p) -' n)) ^ (p | ((len p) -' n))
proof end;

theorem Th5: :: FRIENDS1:5
for k, n being Nat
for p, q being FinSequence st (p /^ k) ^ (p | k) = (q /^ n) ^ (q | n) holds
ex i being Nat st p = (q /^ i) ^ (q | i)
proof end;

scheme :: FRIENDS1:sch 1
Sch{ F1() -> non empty set , F2() -> non zero Nat, P1[ set ] } :
ex C being Cardinal st F2() *` C = card { F where F is Element of F2() -tuples_on F1() : P1[F] }
provided
A1: for p, q being FinSequence of F1() st p ^ q is F2() -element & P1[p ^ q] holds
P1[q ^ p] and
A2: for p being Element of F2() -tuples_on F1() st P1[p] holds
for i being Nat st i < F2() & p = (p /^ i) ^ (p | i) holds
i = 0
proof end;

theorem Th6: :: FRIENDS1:6
for k, n being Nat
for X being non empty set
for A being non empty finite Subset of X
for P being Function of X,(bool X) st ( for x being object 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 being Nat st i in Seg k holds
F . (i + 1) in P . (F . i) ) )
}
= (card A) * (n |^ k)
proof end;

theorem Th7: :: FRIENDS1:7
for p being FinSequence st len p is prime & ex i being Nat st
( 0 < i & i < len p & p = (p /^ i) ^ (p | i) ) holds
rng p c= {(p . 1)}
proof end;

definition
let R be Relation;
let x be Element of field R;
attr x is universal_friend means :Def1: :: FRIENDS1:def 1
for y being object st y in (field R) \ {x} holds
[x,y] in R;
end;

:: deftheorem Def1 defines universal_friend FRIENDS1:def 1 :
for R being Relation
for x being Element of field R holds
( x is universal_friend iff for y being object st y in (field R) \ {x} holds
[x,y] in R );

definition
let R be Relation;
attr R is with_universal_friend means :: FRIENDS1:def 2
ex x being Element of field R st x is universal_friend ;
end;

:: deftheorem defines with_universal_friend FRIENDS1:def 2 :
for R being Relation holds
( R is with_universal_friend iff ex x being Element of field R st x is universal_friend );

notation
let R be Relation;
antonym without_universal_friend R for with_universal_friend ;
end;

definition
let R be Relation;
attr R is friendship_graph_like means :Def3: :: FRIENDS1:def 3
for x, y being object st x in field R & y in field R & x <> y holds
ex z being object st (Im (R,x)) /\ (Coim (R,y)) = {z};
end;

:: deftheorem Def3 defines friendship_graph_like FRIENDS1:def 3 :
for R being Relation holds
( R is friendship_graph_like iff for x, y being object st x in field R & y in field R & x <> y holds
ex z being object st (Im (R,x)) /\ (Coim (R,y)) = {z} );

registration
cluster Relation-like irreflexive symmetric finite friendship_graph_like for set ;
existence
ex b1 being Relation st
( b1 is finite & b1 is symmetric & b1 is irreflexive & b1 is friendship_graph_like )
proof end;
end;

:: WP: Friendship graph
definition
mode Friendship_Graph is irreflexive symmetric finite friendship_graph_like Relation;
end;

Lm5: for x, y, z being object
for P being finite Relation
for t being object st P is friendship_graph_like & x <> y & [x,z] in P & [z,y] in P & [x,t] in P & [t,y] in P holds
z = t

proof end;

theorem Th8: :: FRIENDS1:8
for x being object
for FSG being Friendship_Graph holds 2 divides card (Im (FSG,x))
proof end;

theorem Th9: :: FRIENDS1:9
for x, y being object
for FSG being Friendship_Graph st x in field FSG & y in field FSG & not [x,y] in FSG holds
card (Im (FSG,x)) = card (Im (FSG,y))
proof end;

theorem Th10: :: FRIENDS1:10
for x being object
for FSG being Friendship_Graph st FSG is without_universal_friend & x in field FSG holds
card (Im (FSG,x)) > 2
proof end;

theorem Th11: :: FRIENDS1:11
for x, y being object
for FSG being Friendship_Graph st FSG is without_universal_friend & x in field FSG & y in field FSG holds
card (Im (FSG,x)) = card (Im (FSG,y))
proof end;

theorem Th12: :: FRIENDS1:12
for x being object
for FSG being Friendship_Graph st FSG is without_universal_friend & x in field FSG holds
card (field FSG) = 1 + ((card (Im (FSG,x))) * ((card (Im (FSG,x))) - 1))
proof end;

theorem :: FRIENDS1:13
for FSG being Friendship_Graph
for x, y being 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} )
proof end;

:: WP: Friendship theorem
theorem :: FRIENDS1:14
for FSG being Friendship_Graph st not FSG is empty holds
FSG is with_universal_friend
proof end;