:: 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{ F₁() -> non empty set , F₂() -> non zero Nat, P₁[ set ] } :

ex C being Cardinal st F₂() *` C = card { F where F is Element of F₂() -tuples_on F₁() : P₁[F] }

provided

A1: for p, q being FinSequence of F₁() st p ^ q is F₂() -element & P₁[p ^ q] holds
P₁[q ^ p] and
A2: for p being Element of F₂() -tuples_on F₁() st P₁[p] holds
for i being Nat st i < F₂() & 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 b₁ being Relation st
( b₁ is finite & b₁ is symmetric & b₁ is irreflexive & b₁ is friendship_graph_like )

proof end;

end;

:: 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;

:: Friendship theorem

theorem :: FRIENDS1:14

for FSG being Friendship_Graph st not FSG is empty holds
FSG is with_universal_friend

proof end;