:: About Graph Unions and Intersections
:: by Sebastian Koch
::
:: Received May 19, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users

definition

let X be set ;

attr X is Graph-membered means :Def1: :: GLIB_014:def 1
for x being object st x in X holds
x is _Graph;

end;

:: deftheorem Def1 defines Graph-membered GLIB_014:def 1 :
for X being set holds
( X is Graph-membered iff for x being object st x in X holds
x is _Graph );

registration

cluster empty -> Graph-membered for set ;

coherence
for b₁ being set st b₁ is empty holds
b₁ is Graph-membered ;

end;

registration

let F be Graph-yielding Function;

cluster rng F -> Graph-membered ;

coherence
rng F is Graph-membered

proof end;

end;

registration

let G1 be _Graph;

cluster {G1} -> Graph-membered ;

coherence
{G1} is Graph-membered by TARSKI:def 1;
let G2 be _Graph;

cluster {G1,G2} -> Graph-membered ;

coherence
{G1,G2} is Graph-membered

proof end;

end;

:: there is no functor/mode yet
:: to construct an infinite number of graphs at once

registration

cluster empty Graph-membered for set ;

existence
ex b₁ being set st
( b₁ is empty & b₁ is Graph-membered )

proof end;

cluster non empty trivial finite Graph-membered for set ;

existence
ex b₁ being set st
( b₁ is trivial & b₁ is finite & not b₁ is empty & b₁ is Graph-membered )

proof end;

end;

registration

let X be Graph-membered set ;

cluster -> Graph-membered for Element of K19(X);

coherence
for b₁ being Subset of X holds b₁ is Graph-membered by Def1;

end;

:: the usual set operations preserve graph membership

registration

let X be Graph-membered set ;
let Y be set ;

cluster X /\ Y -> Graph-membered ;

coherence
X /\ Y is Graph-membered

proof end;

cluster X \ Y -> Graph-membered ;

coherence
X \ Y is Graph-membered ;

end;

registration

let X, Y be Graph-membered set ;

cluster X \/ Y -> Graph-membered ;

coherence
X \/ Y is Graph-membered

proof end;

cluster X \+\ Y -> Graph-membered ;

coherence
X \+\ Y is Graph-membered ;

end;

theorem :: GLIB_014:1

for X being set st ( for Y being object st Y in X holds
Y is Graph-membered set ) holds
union X is Graph-membered

proof end;

theorem :: GLIB_014:2

for X being set st ex Y being Graph-membered set st Y in X holds
meet X is Graph-membered

proof end;

registration

let X be non empty Graph-membered set ;

cluster -> Relation-like Function-like for Element of X;

coherence
for b₁ being Element of X holds
( b₁ is Function-like & b₁ is Relation-like ) by Def1;

end;

registration

let X be non empty Graph-membered set ;

cluster -> NAT -defined finite for Element of X;

coherence
for b₁ being Element of X holds
( b₁ is NAT -defined & b₁ is finite ) by Def1;

end;

registration

let X be non empty Graph-membered set ;

cluster -> [Graph-like] for Element of X;

coherence
for b₁ being Element of X holds b₁ is [Graph-like] by Def1;

end;

:: several graphs attributes for sets of graphs
:: ("finite" and "trivial" are deliberately omitted,
:: so that the set attributes are not overridden)

definition

let S be Graph-membered set ;

attr S is plain means :Def2: :: GLIB_014:def 2
for G being _Graph st G in S holds
G is plain ;

attr S is loopless means :Def3: :: GLIB_014:def 3
for G being _Graph st G in S holds
G is loopless ;

attr S is non-multi means :Def4: :: GLIB_014:def 4
for G being _Graph st G in S holds
G is non-multi ;

attr S is non-Dmulti means :Def5: :: GLIB_014:def 5
for G being _Graph st G in S holds
G is non-Dmulti ;

attr S is simple means :: GLIB_014:def 6
for G being _Graph st G in S holds
G is simple ;

attr S is Dsimple means :: GLIB_014:def 7
for G being _Graph st G in S holds
G is Dsimple ;

attr S is acyclic means :Def8: :: GLIB_014:def 8
for G being _Graph st G in S holds
G is acyclic ;

attr S is connected means :Def9: :: GLIB_014:def 9
for G being _Graph st G in S holds
G is connected ;

attr S is Tree-like means :: GLIB_014:def 10
for G being _Graph st G in S holds
G is Tree-like ;

attr S is chordal means :Def11: :: GLIB_014:def 11
for G being _Graph st G in S holds
G is chordal ;

attr S is edgeless means :Def12: :: GLIB_014:def 12
for G being _Graph st G in S holds
G is edgeless ;

attr S is loopfull means :Def13: :: GLIB_014:def 13
for G being _Graph st G in S holds
G is loopfull ;

end;

:: deftheorem Def2 defines plain GLIB_014:def 2 :
for S being Graph-membered set holds
( S is plain iff for G being _Graph st G in S holds
G is plain );

:: deftheorem Def3 defines loopless GLIB_014:def 3 :
for S being Graph-membered set holds
( S is loopless iff for G being _Graph st G in S holds
G is loopless );

:: deftheorem Def4 defines non-multi GLIB_014:def 4 :
for S being Graph-membered set holds
( S is non-multi iff for G being _Graph st G in S holds
G is non-multi );

:: deftheorem Def5 defines non-Dmulti GLIB_014:def 5 :
for S being Graph-membered set holds
( S is non-Dmulti iff for G being _Graph st G in S holds
G is non-Dmulti );

:: deftheorem defines simple GLIB_014:def 6 :
for S being Graph-membered set holds
( S is simple iff for G being _Graph st G in S holds
G is simple );

:: deftheorem defines Dsimple GLIB_014:def 7 :
for S being Graph-membered set holds
( S is Dsimple iff for G being _Graph st G in S holds
G is Dsimple );

:: deftheorem Def8 defines acyclic GLIB_014:def 8 :
for S being Graph-membered set holds
( S is acyclic iff for G being _Graph st G in S holds
G is acyclic );

:: deftheorem Def9 defines connected GLIB_014:def 9 :
for S being Graph-membered set holds
( S is connected iff for G being _Graph st G in S holds
G is connected );

:: deftheorem defines Tree-like GLIB_014:def 10 :
for S being Graph-membered set holds
( S is Tree-like iff for G being _Graph st G in S holds
G is Tree-like );

:: deftheorem Def11 defines chordal GLIB_014:def 11 :
for S being Graph-membered set holds
( S is chordal iff for G being _Graph st G in S holds
G is chordal );

:: deftheorem Def12 defines edgeless GLIB_014:def 12 :
for S being Graph-membered set holds
( S is edgeless iff for G being _Graph st G in S holds
G is edgeless );

:: deftheorem Def13 defines loopfull GLIB_014:def 13 :
for S being Graph-membered set holds
( S is loopfull iff for G being _Graph st G in S holds
G is loopfull );

:: negative clustering are omitted, because
:: negative attributes (e.g. "non-loopless") are not defined yet

registration

cluster empty Graph-membered -> Graph-membered plain loopless non-multi non-Dmulti simple Dsimple acyclic connected Tree-like chordal edgeless loopfull for set ;

coherence
for b₁ being Graph-membered set st b₁ is empty holds
( b₁ is plain & b₁ is loopless & b₁ is non-multi & b₁ is non-Dmulti & b₁ is simple & b₁ is Dsimple & b₁ is acyclic & b₁ is connected & b₁ is Tree-like & b₁ is chordal & b₁ is edgeless & b₁ is loopfull ) ;

cluster Graph-membered non-multi -> Graph-membered non-Dmulti for set ;

coherence
for b₁ being Graph-membered set st b₁ is non-multi holds
b₁ is non-Dmulti

proof end;

cluster Graph-membered loopless non-multi -> Graph-membered simple for set ;

coherence
for b₁ being Graph-membered set st b₁ is loopless & b₁ is non-multi holds
b₁ is simple

proof end;

cluster Graph-membered loopless non-Dmulti -> Graph-membered Dsimple for set ;

coherence
for b₁ being Graph-membered set st b₁ is loopless & b₁ is non-Dmulti holds
b₁ is Dsimple

proof end;

cluster Graph-membered simple -> Graph-membered loopless non-multi for set ;

coherence
for b₁ being Graph-membered set st b₁ is simple holds
( b₁ is loopless & b₁ is non-multi )

proof end;

cluster Graph-membered Dsimple -> Graph-membered loopless non-Dmulti for set ;

coherence
for b₁ being Graph-membered set st b₁ is Dsimple holds
( b₁ is loopless & b₁ is non-Dmulti )

proof end;

cluster Graph-membered acyclic -> Graph-membered simple for set ;

coherence
for b₁ being Graph-membered set st b₁ is acyclic holds
b₁ is simple

proof end;

cluster Graph-membered acyclic connected -> Graph-membered Tree-like for set ;

coherence
for b₁ being Graph-membered set st b₁ is acyclic & b₁ is connected holds
b₁ is Tree-like

proof end;

cluster Graph-membered Tree-like -> Graph-membered acyclic connected for set ;

coherence
for b₁ being Graph-membered set st b₁ is Tree-like holds
( b₁ is acyclic & b₁ is connected )

proof end;

end;

registration

let G1 be plain _Graph;

cluster {G1} -> plain ;

coherence
{G1} is plain by TARSKI:def 1;
let G2 be plain _Graph;

cluster {G1,G2} -> plain ;

coherence
{G1,G2} is plain

proof end;

end;

registration

let G1 be loopless _Graph;

cluster {G1} -> loopless ;

coherence
{G1} is loopless by TARSKI:def 1;
let G2 be loopless _Graph;

cluster {G1,G2} -> loopless ;

coherence
{G1,G2} is loopless

proof end;

end;

registration

let G1 be non-multi _Graph;

cluster {G1} -> non-multi ;

coherence
{G1} is non-multi by TARSKI:def 1;
let G2 be non-multi _Graph;

cluster {G1,G2} -> non-multi ;

coherence
{G1,G2} is non-multi

proof end;

end;

registration

let G1 be non-Dmulti _Graph;

cluster {G1} -> non-Dmulti ;

coherence
{G1} is non-Dmulti by TARSKI:def 1;
let G2 be non-Dmulti _Graph;

cluster {G1,G2} -> non-Dmulti ;

coherence
{G1,G2} is non-Dmulti

proof end;

end;

registration

let G1 be simple _Graph;

cluster {G1} -> simple ;

coherence
{G1} is simple ;
let G2 be simple _Graph;

cluster {G1,G2} -> simple ;

coherence
{G1,G2} is simple ;

end;

registration

let G1 be Dsimple _Graph;

cluster {G1} -> Dsimple ;

coherence
{G1} is Dsimple ;
let G2 be Dsimple _Graph;

cluster {G1,G2} -> Dsimple ;

coherence
{G1,G2} is Dsimple ;

end;

registration

let G1 be acyclic _Graph;

cluster {G1} -> acyclic ;

coherence
{G1} is acyclic by TARSKI:def 1;
let G2 be acyclic _Graph;

cluster {G1,G2} -> acyclic ;

coherence
{G1,G2} is acyclic

proof end;

end;

registration

let G1 be connected _Graph;

cluster {G1} -> connected ;

coherence
{G1} is connected by TARSKI:def 1;
let G2 be connected _Graph;

cluster {G1,G2} -> connected ;

coherence
{G1,G2} is connected

proof end;

end;

registration

let G1 be Tree-like _Graph;

cluster {G1} -> Tree-like ;

coherence
{G1} is Tree-like ;
let G2 be Tree-like _Graph;

cluster {G1,G2} -> Tree-like ;

coherence
{G1,G2} is Tree-like ;

end;

registration

let G1 be chordal _Graph;

cluster {G1} -> chordal ;

coherence
{G1} is chordal by TARSKI:def 1;
let G2 be chordal _Graph;

cluster {G1,G2} -> chordal ;

coherence
{G1,G2} is chordal

proof end;

end;

registration

let G1 be edgeless _Graph;

cluster {G1} -> edgeless ;

coherence
{G1} is edgeless by TARSKI:def 1;
let G2 be edgeless _Graph;

cluster {G1,G2} -> edgeless ;

coherence
{G1,G2} is edgeless

proof end;

end;

registration

let G1 be loopfull _Graph;

cluster {G1} -> loopfull ;

coherence
{G1} is loopfull by TARSKI:def 1;
let G2 be loopfull _Graph;

cluster {G1,G2} -> loopfull ;

coherence
{G1,G2} is loopfull

proof end;

end;

::registration
::let G1 be vertex-finite _Graph;
::cluster {G1} -> vertex-finite;
::coherence;
::let G2 be vertex-finite _Graph;
::cluster {G1, G2} -> vertex-finite;
::coherence;
::end;
::
::registration
::let G1 be edge-finite _Graph;
::cluster {G1} -> edge-finite;
::coherence;
::let G2 be edge-finite _Graph;
::cluster {G1, G2} -> edge-finite;
::coherence;
::end;
:: attributes given through graph yielding functions

theorem Th3: :: GLIB_014:3

for F being Graph-yielding Function holds
( ( F is plain implies rng F is plain ) & ( rng F is plain implies F is plain ) & ( F is loopless implies rng F is loopless ) & ( rng F is loopless implies F is loopless ) & ( F is non-multi implies rng F is non-multi ) & ( rng F is non-multi implies F is non-multi ) & ( F is non-Dmulti implies rng F is non-Dmulti ) & ( rng F is non-Dmulti implies F is non-Dmulti ) & ( F is acyclic implies rng F is acyclic ) & ( rng F is acyclic implies F is acyclic ) & ( F is connected implies rng F is connected ) & ( rng F is connected implies F is connected ) & ( F is chordal implies rng F is chordal ) & ( rng F is chordal implies F is chordal ) & ( F is edgeless implies rng F is edgeless ) & ( rng F is edgeless implies F is edgeless ) & ( F is loopfull implies rng F is loopfull ) & ( rng F is loopfull implies F is loopfull ) )

proof end;

theorem Th4: :: GLIB_014:4

for F being Graph-yielding Function holds
( ( F is simple implies rng F is simple ) & ( rng F is simple implies F is simple ) & ( F is Dsimple implies rng F is Dsimple ) & ( rng F is Dsimple implies F is Dsimple ) & ( F is Tree-like implies rng F is Tree-like ) & ( rng F is Tree-like implies F is Tree-like ) )

proof end;

registration

let F be Graph-yielding plain Function;

cluster rng F -> plain ;

coherence
rng F is plain by Th3;

end;

registration

let F be Graph-yielding loopless Function;

cluster rng F -> loopless ;

coherence
rng F is loopless by Th3;

end;

registration

let F be Graph-yielding non-multi Function;

cluster rng F -> non-multi ;

coherence
rng F is non-multi by Th3;

end;

registration

let F be Graph-yielding non-Dmulti Function;

cluster rng F -> non-Dmulti ;

coherence
rng F is non-Dmulti by Th3;

end;

registration

let F be Graph-yielding simple Function;

cluster rng F -> simple ;

coherence
rng F is simple ;

end;

registration

let F be Graph-yielding Dsimple Function;

cluster rng F -> Dsimple ;

coherence
rng F is Dsimple ;

end;

registration

let F be Graph-yielding acyclic Function;

cluster rng F -> acyclic ;

coherence
rng F is acyclic by Th3;

end;

registration

let F be Graph-yielding connected Function;

cluster rng F -> connected ;

coherence
rng F is connected by Th3;

end;

registration

let F be Graph-yielding Tree-like Function;

cluster rng F -> Tree-like ;

coherence
rng F is Tree-like ;

end;

registration

let F be Graph-yielding chordal Function;

cluster rng F -> chordal ;

coherence
rng F is chordal by Th3;

end;

registration

let F be Graph-yielding edgeless Function;

cluster rng F -> edgeless ;

coherence
rng F is edgeless by Th3;

end;

registration

let F be Graph-yielding loopfull Function;

cluster rng F -> loopfull ;

coherence
rng F is loopfull by Th3;

end;

::registration
::let F be vertex-finite Graph-yielding Function;
::cluster rng F -> vertex-finite;
::coherence
::proof
::let G be _Graph;
::assume G in rng F;
::then consider x being object such that
::A1: x in dom F & F.x = G by FUNCT_1:def 3;
::consider G0 being _Graph such that
::A2: F.x = G0 & G0 is vertex-finite by A1, GLIB_012:def 2;
::thus G is vertex-finite by A1, A2;
::end;
::end;
::
::registration
::let F be edge-finite Graph-yielding Function;
::cluster rng F -> edge-finite;
::coherence
::proof
::let G be _Graph;
::assume G in rng F;
::then consider x being object such that
::A1: x in dom F & F.x = G by FUNCT_1:def 3;
::consider G0 being _Graph such that
::A2: F.x = G0 & G0 is edge-finite by A1, GLIB_012:def 2;
::thus G is edge-finite by A1, A2;
::end;
::end;
:: attributes of graph subsets

registration

let X be Graph-membered plain set ;

cluster -> plain for Element of K19(X);

coherence
for b₁ being Subset of X holds b₁ is plain by Def2;

end;

registration

let X be Graph-membered loopless set ;

cluster -> loopless for Element of K19(X);

coherence
for b₁ being Subset of X holds b₁ is loopless by Def3;

end;

registration

let X be Graph-membered non-multi set ;

cluster -> non-multi for Element of K19(X);

coherence
for b₁ being Subset of X holds b₁ is non-multi by Def4;

end;

registration

let X be Graph-membered non-Dmulti set ;

cluster -> non-Dmulti for Element of K19(X);

coherence
for b₁ being Subset of X holds b₁ is non-Dmulti by Def5;

end;

registration

let X be Graph-membered simple set ;

cluster -> simple for Element of K19(X);

coherence
for b₁ being Subset of X holds b₁ is simple ;

end;

registration

let X be Graph-membered Dsimple set ;

cluster -> Dsimple for Element of K19(X);

coherence
for b₁ being Subset of X holds b₁ is Dsimple ;

end;

registration

let X be Graph-membered acyclic set ;

cluster -> acyclic for Element of K19(X);

coherence
for b₁ being Subset of X holds b₁ is acyclic by Def8;

end;

registration

let X be Graph-membered connected set ;

cluster -> connected for Element of K19(X);

coherence
for b₁ being Subset of X holds b₁ is connected by Def9;

end;

registration

let X be Graph-membered Tree-like set ;

cluster -> Tree-like for Element of K19(X);

coherence
for b₁ being Subset of X holds b₁ is Tree-like ;

end;

registration

let X be Graph-membered chordal set ;

cluster -> chordal for Element of K19(X);

coherence
for b₁ being Subset of X holds b₁ is chordal by Def11;

end;

registration

let X be Graph-membered edgeless set ;

cluster -> edgeless for Element of K19(X);

coherence
for b₁ being Subset of X holds b₁ is edgeless by Def12;

end;

registration

let X be Graph-membered loopfull set ;

cluster -> loopfull for Element of K19(X);

coherence
for b₁ being Subset of X holds b₁ is loopfull by Def13;

end;

::registration
::let X be vertex-finite Graph-membered set;
::cluster -> vertex-finite for Subset of X;
::coherence by Def16;
::end;
::
::registration
::let X be edge-finite Graph-membered set;
::cluster -> edge-finite for Subset of X;
::coherence by Def16;
::end;
:: attributes of graph sets and set operations

registration

let X be Graph-membered plain set ;
let Y be set ;

cluster X /\ Y -> plain ;

coherence
X /\ Y is plain

proof end;

cluster X \ Y -> plain ;

coherence
X \ Y is plain ;

end;

registration

let X, Y be Graph-membered plain set ;

cluster X \/ Y -> plain ;

coherence
X \/ Y is plain

proof end;

cluster X \+\ Y -> plain ;

coherence
X \+\ Y is plain ;

end;

registration

let X be Graph-membered loopless set ;
let Y be set ;

cluster X /\ Y -> loopless ;

coherence
X /\ Y is loopless

proof end;

cluster X \ Y -> loopless ;

coherence
X \ Y is loopless ;

end;

registration

let X, Y be Graph-membered loopless set ;

cluster X \/ Y -> loopless ;

coherence
X \/ Y is loopless

proof end;

cluster X \+\ Y -> loopless ;

coherence
X \+\ Y is loopless ;

end;

registration

let X be Graph-membered non-multi set ;
let Y be set ;

cluster X /\ Y -> non-multi ;

coherence
X /\ Y is non-multi

proof end;

cluster X \ Y -> non-multi ;

coherence
X \ Y is non-multi ;

end;

registration

let X, Y be Graph-membered non-multi set ;

cluster X \/ Y -> non-multi ;

coherence
X \/ Y is non-multi

proof end;

cluster X \+\ Y -> non-multi ;

coherence
X \+\ Y is non-multi ;

end;

registration

let X be Graph-membered non-Dmulti set ;
let Y be set ;

cluster X /\ Y -> non-Dmulti ;

coherence
X /\ Y is non-Dmulti

proof end;

cluster X \ Y -> non-Dmulti ;

coherence
X \ Y is non-Dmulti ;

end;

registration

let X, Y be Graph-membered non-Dmulti set ;

cluster X \/ Y -> non-Dmulti ;

coherence
X \/ Y is non-Dmulti

proof end;

cluster X \+\ Y -> non-Dmulti ;

coherence
X \+\ Y is non-Dmulti ;

end;

registration

let X be Graph-membered simple set ;
let Y be set ;

cluster X /\ Y -> simple ;

coherence
X /\ Y is simple ;

cluster X \ Y -> simple ;

coherence
X \ Y is simple ;

end;

registration

let X, Y be Graph-membered simple set ;

cluster X \/ Y -> simple ;

coherence
X \/ Y is simple ;

cluster X \+\ Y -> simple ;

coherence
X \+\ Y is simple ;

end;

registration

let X be Graph-membered Dsimple set ;
let Y be set ;

cluster X /\ Y -> Dsimple ;

coherence
X /\ Y is Dsimple ;

cluster X \ Y -> Dsimple ;

coherence
X \ Y is Dsimple ;

end;

registration

let X, Y be Graph-membered Dsimple set ;

cluster X \/ Y -> Dsimple ;

coherence
X \/ Y is Dsimple ;

cluster X \+\ Y -> Dsimple ;

coherence
X \+\ Y is Dsimple ;

end;

registration

let X be Graph-membered acyclic set ;
let Y be set ;

cluster X /\ Y -> acyclic ;

coherence
X /\ Y is acyclic

proof end;

cluster X \ Y -> acyclic ;

coherence
X \ Y is acyclic ;

end;

registration

let X, Y be Graph-membered acyclic set ;

cluster X \/ Y -> acyclic ;

coherence
X \/ Y is acyclic

proof end;

cluster X \+\ Y -> acyclic ;

coherence
X \+\ Y is acyclic ;

end;

registration

let X be Graph-membered connected set ;
let Y be set ;

cluster X /\ Y -> connected ;

coherence
X /\ Y is connected

proof end;

cluster X \ Y -> connected ;

coherence
X \ Y is connected ;

end;

registration

let X, Y be Graph-membered connected set ;

cluster X \/ Y -> connected ;

coherence
X \/ Y is connected

proof end;

cluster X \+\ Y -> connected ;

coherence
X \+\ Y is connected ;

end;

registration

let X be Graph-membered Tree-like set ;
let Y be set ;

cluster X /\ Y -> Tree-like ;

coherence
X /\ Y is Tree-like ;

cluster X \ Y -> Tree-like ;

coherence
X \ Y is Tree-like ;

end;

registration

let X, Y be Graph-membered Tree-like set ;

cluster X \/ Y -> Tree-like ;

coherence
X \/ Y is Tree-like ;

cluster X \+\ Y -> Tree-like ;

coherence
X \+\ Y is Tree-like ;

end;

registration

let X be Graph-membered chordal set ;
let Y be set ;

cluster X /\ Y -> chordal ;

coherence
X /\ Y is chordal

proof end;

cluster X \ Y -> chordal ;

coherence
X \ Y is chordal ;

end;

registration

let X, Y be Graph-membered chordal set ;

cluster X \/ Y -> chordal ;

coherence
X \/ Y is chordal

proof end;

cluster X \+\ Y -> chordal ;

coherence
X \+\ Y is chordal ;

end;

registration

let X be Graph-membered edgeless set ;
let Y be set ;

cluster X /\ Y -> edgeless ;

coherence
X /\ Y is edgeless

proof end;

cluster X \ Y -> edgeless ;

coherence
X \ Y is edgeless ;

end;

registration

let X, Y be Graph-membered edgeless set ;

cluster X \/ Y -> edgeless ;

coherence
X \/ Y is edgeless

proof end;

cluster X \+\ Y -> edgeless ;

coherence
X \+\ Y is edgeless ;

end;

registration

let X be Graph-membered loopfull set ;
let Y be set ;

cluster X /\ Y -> loopfull ;

coherence
X /\ Y is loopfull

proof end;

cluster X \ Y -> loopfull ;

coherence
X \ Y is loopfull ;

end;

registration

let X, Y be Graph-membered loopfull set ;

cluster X \/ Y -> loopfull ;

coherence
X \/ Y is loopfull

proof end;

cluster X \+\ Y -> loopfull ;

coherence
X \+\ Y is loopfull ;

end;

::registration
::let X be vertex-finite Graph-membered set, Y be set;
::cluster X /\ Y -> vertex-finite;
::coherence
::proof
::X /\ Y c= X by XBOOLE_1:17;
::hence thesis;
::end;
::cluster X \ Y -> vertex-finite;
::coherence;
::end;
::
::registration
::let X, Y be vertex-finite Graph-membered set;
::cluster X \/ Y -> vertex-finite;
::coherence
::proof
::let x be _Graph;
::assume x in X \/ Y;
::then per cases by XBOOLE_0:def 3;
::suppose x in X;
::hence thesis by Def16;
::end;
::suppose x in Y;
::hence thesis by Def16;
::end;
::end;
::cluster X \+\ Y -> vertex-finite;
::coherence
::proof
::X \+\ Y = (X \ Y) \/ (Y \ X) by XBOOLE_0:def 6;
::hence thesis;
::end;
::end;
::
::registration
::let X be edge-finite Graph-membered set, Y be set;
::cluster X /\ Y -> edge-finite;
::coherence
::proof
::X /\ Y c= X by XBOOLE_1:17;
::hence thesis;
::end;
::cluster X \ Y -> edge-finite;
::coherence;
::end;
::
::registration
::let X, Y be edge-finite Graph-membered set;
::cluster X \/ Y -> edge-finite;
::coherence
::proof
::let x be _Graph;
::assume x in X \/ Y;
::then per cases by XBOOLE_0:def 3;
::suppose x in X;
::hence thesis by Def16;
::end;
::suppose x in Y;
::hence thesis by Def16;
::end;
::end;
::cluster X \+\ Y -> edge-finite;
::coherence
::proof
::X \+\ Y = (X \ Y) \/ (Y \ X) by XBOOLE_0:def 6;
::hence thesis;
::end;
::end;
:: existence clusters for all attributes

registration

cluster empty Graph-membered plain loopless non-multi non-Dmulti simple Dsimple acyclic connected Tree-like chordal edgeless loopfull for set ;

existence
ex b₁ being Graph-membered set st
( b₁ is empty & b₁ is plain & b₁ is loopless & b₁ is non-multi & b₁ is non-Dmulti & b₁ is simple & b₁ is Dsimple & b₁ is acyclic & b₁ is connected & b₁ is Tree-like & b₁ is chordal & b₁ is edgeless & b₁ is loopfull )

proof end;

cluster non empty Graph-membered loopless non-multi non-Dmulti simple Dsimple acyclic connected Tree-like for set ;

existence
ex b₁ being Graph-membered set st
( not b₁ is empty & b₁ is Tree-like & b₁ is acyclic & b₁ is connected & b₁ is simple & b₁ is Dsimple & b₁ is loopless & b₁ is non-multi & b₁ is non-Dmulti )

proof end;

cluster non empty Graph-membered chordal edgeless for set ;

existence
ex b₁ being Graph-membered set st
( not b₁ is empty & b₁ is edgeless & b₁ is chordal )

proof end;

cluster non empty Graph-membered loopfull for set ;

existence
ex b₁ being Graph-membered set st
( not b₁ is empty & b₁ is loopfull )

proof end;

cluster non empty Graph-membered plain for set ;

existence
ex b₁ being Graph-membered set st
( not b₁ is empty & b₁ is plain )

proof end;

end;

registration

let S be non empty Graph-membered plain set ;

cluster -> plain for Element of S;

coherence
for b₁ being Element of S holds b₁ is plain by Def2;

end;

registration

let S be non empty Graph-membered loopless set ;

cluster -> loopless for Element of S;

coherence
for b₁ being Element of S holds b₁ is loopless by Def3;

end;

registration

let S be non empty Graph-membered non-multi set ;

cluster -> non-multi for Element of S;

coherence
for b₁ being Element of S holds b₁ is non-multi by Def4;

end;

registration

let S be non empty Graph-membered non-Dmulti set ;

cluster -> non-Dmulti for Element of S;

coherence
for b₁ being Element of S holds b₁ is non-Dmulti by Def5;

end;

registration

let S be non empty Graph-membered simple set ;

cluster -> simple for Element of S;

coherence
for b₁ being Element of S holds b₁ is simple ;

end;

registration

let S be non empty Graph-membered Dsimple set ;

cluster -> Dsimple for Element of S;

coherence
for b₁ being Element of S holds b₁ is Dsimple ;

end;

registration

let S be non empty Graph-membered acyclic set ;

cluster -> acyclic for Element of S;

coherence
for b₁ being Element of S holds b₁ is acyclic by Def8;

end;

registration

let S be non empty Graph-membered connected set ;

cluster -> connected for Element of S;

coherence
for b₁ being Element of S holds b₁ is connected by Def9;

end;

registration

let S be non empty Graph-membered Tree-like set ;

cluster -> Tree-like for Element of S;

coherence
for b₁ being Element of S holds b₁ is Tree-like ;

end;

registration

let S be non empty Graph-membered chordal set ;

cluster -> chordal for Element of S;

coherence
for b₁ being Element of S holds b₁ is chordal by Def11;

end;

registration

let S be non empty Graph-membered edgeless set ;

cluster -> edgeless for Element of S;

coherence
for b₁ being Element of S holds b₁ is edgeless by Def12;

end;

registration

let S be non empty Graph-membered loopfull set ;

cluster -> loopfull for Element of S;

coherence
for b₁ being Element of S holds b₁ is loopfull by Def13;

end;

::registration
::let S be non empty vertex-finite Graph-membered set;
::cluster -> vertex-finite for Element of S;
::coherence by Def16;
::end;
::
::registration
::let S be non empty edge-finite Graph-membered set;
::cluster -> edge-finite for Element of S;
::coherence by Def16;
::end;
:: getting vertices/edges/sources/targets from the Graph-membered set

definition

let S be Graph-membered set ;

func the_Vertices_of S -> set means :Def14: :: GLIB_014:def 14
for V being object holds
( V in it iff ex G being _Graph st
( G in S & V = the_Vertices_of G ) );

existence
ex b₁ being set st
for V being object holds
( V in b₁ iff ex G being _Graph st
( G in S & V = the_Vertices_of G ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for V being object holds
( V in b₁ iff ex G being _Graph st
( G in S & V = the_Vertices_of G ) ) ) & ( for V being object holds
( V in b₂ iff ex G being _Graph st
( G in S & V = the_Vertices_of G ) ) ) holds
b₁ = b₂

proof end;

func the_Edges_of S -> set means :Def15: :: GLIB_014:def 15
for E being object holds
( E in it iff ex G being _Graph st
( G in S & E = the_Edges_of G ) );

existence
ex b₁ being set st
for E being object holds
( E in b₁ iff ex G being _Graph st
( G in S & E = the_Edges_of G ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for E being object holds
( E in b₁ iff ex G being _Graph st
( G in S & E = the_Edges_of G ) ) ) & ( for E being object holds
( E in b₂ iff ex G being _Graph st
( G in S & E = the_Edges_of G ) ) ) holds
b₁ = b₂

proof end;

func the_Source_of S -> set means :Def16: :: GLIB_014:def 16
for s being object holds
( s in it iff ex G being _Graph st
( G in S & s = the_Source_of G ) );

existence
ex b₁ being set st
for s being object holds
( s in b₁ iff ex G being _Graph st
( G in S & s = the_Source_of G ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for s being object holds
( s in b₁ iff ex G being _Graph st
( G in S & s = the_Source_of G ) ) ) & ( for s being object holds
( s in b₂ iff ex G being _Graph st
( G in S & s = the_Source_of G ) ) ) holds
b₁ = b₂

proof end;

func the_Target_of S -> set means :Def17: :: GLIB_014:def 17
for t being object holds
( t in it iff ex G being _Graph st
( G in S & t = the_Target_of G ) );

existence
ex b₁ being set st
for t being object holds
( t in b₁ iff ex G being _Graph st
( G in S & t = the_Target_of G ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for t being object holds
( t in b₁ iff ex G being _Graph st
( G in S & t = the_Target_of G ) ) ) & ( for t being object holds
( t in b₂ iff ex G being _Graph st
( G in S & t = the_Target_of G ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def14 defines the_Vertices_of GLIB_014:def 14 :
for S being Graph-membered set
for b₂ being set holds
( b₂ = the_Vertices_of S iff for V being object holds
( V in b₂ iff ex G being _Graph st
( G in S & V = the_Vertices_of G ) ) );

:: deftheorem Def15 defines the_Edges_of GLIB_014:def 15 :
for S being Graph-membered set
for b₂ being set holds
( b₂ = the_Edges_of S iff for E being object holds
( E in b₂ iff ex G being _Graph st
( G in S & E = the_Edges_of G ) ) );

:: deftheorem Def16 defines the_Source_of GLIB_014:def 16 :
for S being Graph-membered set
for b₂ being set holds
( b₂ = the_Source_of S iff for s being object holds
( s in b₂ iff ex G being _Graph st
( G in S & s = the_Source_of G ) ) );

:: deftheorem Def17 defines the_Target_of GLIB_014:def 17 :
for S being Graph-membered set
for b₂ being set holds
( b₂ = the_Target_of S iff for t being object holds
( t in b₂ iff ex G being _Graph st
( G in S & t = the_Target_of G ) ) );

definition

let S be non empty Graph-membered set ;

redefine func the_Vertices_of S equals :: GLIB_014:def 18
{ (the_Vertices_of G) where G is Element of S : verum } ;

compatibility
for b₁ being set holds
( b₁ = the_Vertices_of S iff b₁ = { (the_Vertices_of G) where G is Element of S : verum } )

proof end;

redefine func the_Edges_of S equals :: GLIB_014:def 19
{ (the_Edges_of G) where G is Element of S : verum } ;

compatibility
for b₁ being set holds
( b₁ = the_Edges_of S iff b₁ = { (the_Edges_of G) where G is Element of S : verum } )

proof end;

redefine func the_Source_of S equals :: GLIB_014:def 20
{ (the_Source_of G) where G is Element of S : verum } ;

compatibility
for b₁ being set holds
( b₁ = the_Source_of S iff b₁ = { (the_Source_of G) where G is Element of S : verum } )

proof end;

redefine func the_Target_of S equals :: GLIB_014:def 21
{ (the_Target_of G) where G is Element of S : verum } ;

compatibility
for b₁ being set holds
( b₁ = the_Target_of S iff b₁ = { (the_Target_of G) where G is Element of S : verum } )

proof end;

end;

:: deftheorem defines the_Vertices_of GLIB_014:def 18 :
for S being non empty Graph-membered set holds the_Vertices_of S = { (the_Vertices_of G) where G is Element of S : verum } ;

:: deftheorem defines the_Edges_of GLIB_014:def 19 :
for S being non empty Graph-membered set holds the_Edges_of S = { (the_Edges_of G) where G is Element of S : verum } ;

:: deftheorem defines the_Source_of GLIB_014:def 20 :
for S being non empty Graph-membered set holds the_Source_of S = { (the_Source_of G) where G is Element of S : verum } ;

:: deftheorem defines the_Target_of GLIB_014:def 21 :
for S being non empty Graph-membered set holds the_Target_of S = { (the_Target_of G) where G is Element of S : verum } ;

registration

let S be non empty Graph-membered set ;

cluster union (the_Vertices_of S) -> non empty ;

coherence
not union (the_Vertices_of S) is empty

proof end;

end;

registration

let S be Graph-membered set ;

cluster the_Source_of S -> functional ;

coherence
the_Source_of S is functional

proof end;

cluster the_Target_of S -> functional ;

coherence
the_Target_of S is functional

proof end;

end;

registration

let S be empty Graph-membered set ;

cluster the_Vertices_of S -> empty ;

coherence
the_Vertices_of S is empty

proof end;

cluster the_Edges_of S -> empty ;

coherence
the_Edges_of S is empty

proof end;

cluster the_Source_of S -> empty ;

coherence
the_Source_of S is empty

proof end;

cluster the_Target_of S -> empty ;

coherence
the_Target_of S is empty

proof end;

end;

registration

let S be non empty Graph-membered set ;

cluster the_Vertices_of S -> non empty ;

coherence
not the_Vertices_of S is empty

proof end;

cluster the_Edges_of S -> non empty ;

coherence
not the_Edges_of S is empty

proof end;

cluster the_Source_of S -> non empty ;

coherence
not the_Source_of S is empty

proof end;

cluster the_Target_of S -> non empty ;

coherence
not the_Target_of S is empty

proof end;

end;

registration

let S be trivial Graph-membered set ;

cluster the_Vertices_of S -> trivial ;

coherence
the_Vertices_of S is trivial

proof end;

cluster the_Edges_of S -> trivial ;

coherence
the_Edges_of S is trivial

proof end;

cluster the_Source_of S -> trivial ;

coherence
the_Source_of S is trivial

proof end;

cluster the_Target_of S -> trivial ;

coherence
the_Target_of S is trivial

proof end;

end;

theorem Th5: :: GLIB_014:5

for G being _Graph holds
( the_Vertices_of {G} = {(the_Vertices_of G)} & the_Edges_of {G} = {(the_Edges_of G)} & the_Source_of {G} = {(the_Source_of G)} & the_Target_of {G} = {(the_Target_of G)} )

proof end;

theorem Th6: :: GLIB_014:6

for G, H being _Graph holds
( the_Vertices_of {G,H} = {(the_Vertices_of G),(the_Vertices_of H)} & the_Edges_of {G,H} = {(the_Edges_of G),(the_Edges_of H)} & the_Source_of {G,H} = {(the_Source_of G),(the_Source_of H)} & the_Target_of {G,H} = {(the_Target_of G),(the_Target_of H)} )

proof end;

theorem Th7: :: GLIB_014:7

for S being Graph-membered set holds
( card (the_Vertices_of S) c= card S & card (the_Edges_of S) c= card S & card (the_Source_of S) c= card S & card (the_Target_of S) c= card S )

proof end;

registration

let S be finite Graph-membered set ;

cluster the_Vertices_of S -> finite ;

coherence
the_Vertices_of S is finite

proof end;

cluster the_Edges_of S -> finite ;

coherence
the_Edges_of S is finite

proof end;

cluster the_Source_of S -> finite ;

coherence
the_Source_of S is finite

proof end;

cluster the_Target_of S -> finite ;

coherence
the_Target_of S is finite

proof end;

end;

registration

let S be Graph-membered edgeless set ;

cluster union (the_Edges_of S) -> empty ;

coherence
union (the_Edges_of S) is empty

proof end;

end;

theorem Th8: :: GLIB_014:8

for S1, S2 being Graph-membered set holds
( the_Vertices_of (S1 \/ S2) = (the_Vertices_of S1) \/ (the_Vertices_of S2) & the_Edges_of (S1 \/ S2) = (the_Edges_of S1) \/ (the_Edges_of S2) & the_Source_of (S1 \/ S2) = (the_Source_of S1) \/ (the_Source_of S2) & the_Target_of (S1 \/ S2) = (the_Target_of S1) \/ (the_Target_of S2) )

proof end;

:: no equality, for example take {G},{H} with G == H but G <> H

theorem :: GLIB_014:9

for S1, S2 being Graph-membered set holds
( the_Vertices_of (S1 /\ S2) c= (the_Vertices_of S1) /\ (the_Vertices_of S2) & the_Edges_of (S1 /\ S2) c= (the_Edges_of S1) /\ (the_Edges_of S2) & the_Source_of (S1 /\ S2) c= (the_Source_of S1) /\ (the_Source_of S2) & the_Target_of (S1 /\ S2) c= (the_Target_of S1) /\ (the_Target_of S2) )

proof end;

theorem Th10: :: GLIB_014:10

for S1, S2 being Graph-membered set holds
( (the_Vertices_of S1) \ (the_Vertices_of S2) c= the_Vertices_of (S1 \ S2) & (the_Edges_of S1) \ (the_Edges_of S2) c= the_Edges_of (S1 \ S2) & (the_Source_of S1) \ (the_Source_of S2) c= the_Source_of (S1 \ S2) & (the_Target_of S1) \ (the_Target_of S2) c= the_Target_of (S1 \ S2) )

proof end;

theorem :: GLIB_014:11

for S1, S2 being Graph-membered set holds
( (the_Vertices_of S1) \+\ (the_Vertices_of S2) c= the_Vertices_of (S1 \+\ S2) & (the_Edges_of S1) \+\ (the_Edges_of S2) c= the_Edges_of (S1 \+\ S2) & (the_Source_of S1) \+\ (the_Source_of S2) c= the_Source_of (S1 \+\ S2) & (the_Target_of S1) \+\ (the_Target_of S2) c= the_Target_of (S1 \+\ S2) )

proof end;

definition

let G1, G2 be _Graph;

pred G1 tolerates G2 means :: GLIB_014:def 22
( the_Source_of G1 tolerates the_Source_of G2 & the_Target_of G1 tolerates the_Target_of G2 );

reflexivity
for G1 being _Graph holds
( the_Source_of G1 tolerates the_Source_of G1 & the_Target_of G1 tolerates the_Target_of G1 ) ;
symmetry
for G1, G2 being _Graph st the_Source_of G1 tolerates the_Source_of G2 & the_Target_of G1 tolerates the_Target_of G2 holds
( the_Source_of G2 tolerates the_Source_of G1 & the_Target_of G2 tolerates the_Target_of G1 ) ;

end;

:: deftheorem defines tolerates GLIB_014:def 22 :
for G1, G2 being _Graph holds
( G1 tolerates G2 iff ( the_Source_of G1 tolerates the_Source_of G2 & the_Target_of G1 tolerates the_Target_of G2 ) );

theorem Th12: :: GLIB_014:12

for G1, G2 being _Graph st the_Edges_of G1 misses the_Edges_of G2 holds
G1 tolerates G2

proof end;

theorem :: GLIB_014:13

for G1, G2 being _Graph st the_Source_of G1 c= the_Source_of G2 & the_Target_of G1 c= the_Target_of G2 holds
G1 tolerates G2 by PARTFUN1:54;

theorem Th14: :: GLIB_014:14

for G1 being _Graph
for G2, G3 being Subgraph of G1 holds G2 tolerates G3

proof end;

theorem Th15: :: GLIB_014:15

for G1 being _Graph
for G2 being Subgraph of G1 holds G1 tolerates G2

proof end;

theorem :: GLIB_014:16

for G1, G2 being _Graph st G1 == G2 holds
G1 tolerates G2

proof end;

theorem Th17: :: GLIB_014:17

for G1, G2 being _Graph holds
( G1 tolerates G2 iff for e, v1, w1, v2, w2 being object st e DJoins v1,w1,G1 & e DJoins v2,w2,G2 holds
( v1 = v2 & w1 = w2 ) )

proof end;

theorem :: GLIB_014:18

for G1 being _Graph
for E being Subset of (the_Edges_of G1)
for G2 being reverseEdgeDirections of G1,E holds
( G1 tolerates G2 iff E c= G1 .loops() )

proof end;

definition

let S be Graph-membered set ;

attr S is \/-tolerating means :Def23: :: GLIB_014:def 23
for G1, G2 being _Graph st G1 in S & G2 in S holds
G1 tolerates G2;

end;

:: deftheorem Def23 defines \/-tolerating GLIB_014:def 23 :
for S being Graph-membered set holds
( S is \/-tolerating iff for G1, G2 being _Graph st G1 in S & G2 in S holds
G1 tolerates G2 );

definition

let S be non empty Graph-membered set ;

redefine attr S is \/-tolerating means :: GLIB_014:def 24
for G1, G2 being Element of S holds G1 tolerates G2;

compatibility
( S is \/-tolerating iff for G1, G2 being Element of S holds G1 tolerates G2 ) ;

end;

:: deftheorem defines \/-tolerating GLIB_014:def 24 :
for S being non empty Graph-membered set holds
( S is \/-tolerating iff for G1, G2 being Element of S holds G1 tolerates G2 );

registration

cluster empty Graph-membered -> Graph-membered \/-tolerating for set ;

coherence
for b₁ being Graph-membered set st b₁ is empty holds
b₁ is \/-tolerating ;
let G be _Graph;

cluster {G} -> \/-tolerating ;

coherence
{G} is \/-tolerating

proof end;

end;

registration

cluster non empty Graph-membered \/-tolerating for set ;

existence
ex b₁ being Graph-membered set st
( not b₁ is empty & b₁ is \/-tolerating )

proof end;

end;

definition

mode GraphUnionSet is non empty Graph-membered \/-tolerating set ;

end;

theorem Th19: :: GLIB_014:19

for G1, G2 being _Graph holds
( G1 tolerates G2 iff {G1,G2} is \/-tolerating )

proof end;

registration

let S1 be Graph-membered \/-tolerating set ;
let S2 be set ;

cluster S1 /\ S2 -> \/-tolerating ;

coherence
S1 /\ S2 is \/-tolerating

proof end;

cluster S1 \ S2 -> \/-tolerating ;

coherence
S1 \ S2 is \/-tolerating by Def23;

end;

theorem Th20: :: GLIB_014:20

for S1, S2 being Graph-membered set st S1 \/ S2 is \/-tolerating holds
( S1 is \/-tolerating & S2 is \/-tolerating )

proof end;

registration

let S be Graph-membered \/-tolerating set ;

cluster the_Source_of S -> compatible ;

coherence
the_Source_of S is compatible

proof end;

cluster the_Target_of S -> compatible ;

coherence
the_Target_of S is compatible

proof end;

end;

registration

let S be Graph-membered \/-tolerating set ;

cluster union (the_Source_of S) -> Relation-like Function-like ;

coherence
( union (the_Source_of S) is Function-like & union (the_Source_of S) is Relation-like ) ;

cluster union (the_Target_of S) -> Relation-like Function-like ;

coherence
( union (the_Target_of S) is Function-like & union (the_Target_of S) is Relation-like ) ;

end;

registration

let S be Graph-membered \/-tolerating set ;

cluster union (the_Source_of S) -> union (the_Edges_of S) -defined union (the_Vertices_of S) -valued ;

coherence
( union (the_Source_of S) is union (the_Edges_of S) -defined & union (the_Source_of S) is union (the_Vertices_of S) -valued )

proof end;

cluster union (the_Target_of S) -> union (the_Edges_of S) -defined union (the_Vertices_of S) -valued ;

coherence
( union (the_Target_of S) is union (the_Edges_of S) -defined & union (the_Target_of S) is union (the_Vertices_of S) -valued )

proof end;

end;

registration

let S be Graph-membered \/-tolerating set ;

cluster union (the_Source_of S) -> total ;

coherence
union (the_Source_of S) is total

proof end;

cluster union (the_Target_of S) -> total ;

coherence
union (the_Target_of S) is total

proof end;

end;

definition

let S be GraphUnionSet;

mode GraphUnion of S -> _Graph means :Def25: :: GLIB_014:def 25
( the_Vertices_of it = union (the_Vertices_of S) & the_Edges_of it = union (the_Edges_of S) & the_Source_of it = union (the_Source_of S) & the_Target_of it = union (the_Target_of S) );

existence
ex b₁ being _Graph st
( the_Vertices_of b₁ = union (the_Vertices_of S) & the_Edges_of b₁ = union (the_Edges_of S) & the_Source_of b₁ = union (the_Source_of S) & the_Target_of b₁ = union (the_Target_of S) )

proof end;

end;

:: deftheorem Def25 defines GraphUnion GLIB_014:def 25 :
for S being GraphUnionSet
for b₂ being _Graph holds
( b₂ is GraphUnion of S iff ( the_Vertices_of b₂ = union (the_Vertices_of S) & the_Edges_of b₂ = union (the_Edges_of S) & the_Source_of b₂ = union (the_Source_of S) & the_Target_of b₂ = union (the_Target_of S) ) );

:: not really needed
::definition
::let S be GraphUnionSet;
::func union S equals the plain GraphUnion of S;
::end;
:: not proven here (DOMS from VALUED_2)
:: theorem
:: for S being GraphUnionSet, G being GraphUnion of S
:: holds DOMS(the_Source_of S) = dom the_Source_of G &
:: DOMS(the_Target_of S) = dom the_Target_of G;

theorem Th21: :: GLIB_014:21

for S being GraphUnionSet
for G being GraphUnion of S
for H being Element of S holds H is Subgraph of G

proof end;

theorem Th22: :: GLIB_014:22

for S being GraphUnionSet
for G being GraphUnion of S
for G9 being _Graph holds
( G9 is GraphUnion of S iff G == G9 )

proof end;

registration

let S be GraphUnionSet;

cluster Relation-like NAT -defined Function-like finite [Graph-like] plain for GraphUnion of S;

existence
ex b₁ being GraphUnion of S st b₁ is plain

proof end;

end;

registration

cluster non empty Graph-membered loopless \/-tolerating for set ;

existence
ex b₁ being GraphUnionSet st b₁ is loopless

proof end;

cluster non empty Graph-membered edgeless \/-tolerating for set ;

existence
ex b₁ being GraphUnionSet st b₁ is edgeless

proof end;

cluster non empty Graph-membered loopfull \/-tolerating for set ;

existence
ex b₁ being GraphUnionSet st b₁ is loopfull

proof end;

end;

theorem Th23: :: GLIB_014:23

for S being GraphUnionSet
for G being GraphUnion of S holds
( ( S is loopless implies G is loopless ) & ( G is loopless implies S is loopless ) & ( S is edgeless implies G is edgeless ) & ( G is edgeless implies S is edgeless ) & ( S is loopfull implies G is loopfull ) )

proof end;

registration

let S be loopless GraphUnionSet;

cluster -> loopless for GraphUnion of S;

coherence
for b₁ being GraphUnion of S holds b₁ is loopless by Th23;

end;

registration

let S be edgeless GraphUnionSet;

cluster -> edgeless for GraphUnion of S;

coherence
for b₁ being GraphUnion of S holds b₁ is edgeless by Th23;

end;

registration

let S be loopfull GraphUnionSet;

cluster -> loopfull for GraphUnion of S;

coherence
for b₁ being GraphUnion of S holds b₁ is loopfull by Th23;

end;

theorem :: GLIB_014:24

for G, H being _Graph holds
( G is GraphUnion of {H} iff G == H )

proof end;

definition

let G1, G2 be _Graph;

mode GraphUnion of G1,G2 -> Supergraph of G1 means :Def26: :: GLIB_014:def 26
ex S being GraphUnionSet st
( S = {G1,G2} & it is GraphUnion of S ) if G1 tolerates G2
otherwise it == G1;

existence
( ( G1 tolerates G2 implies ex b₁ being Supergraph of G1 ex S being GraphUnionSet st
( S = {G1,G2} & b₁ is GraphUnion of S ) ) & ( not G1 tolerates G2 implies ex b₁ being Supergraph of G1 st b₁ == G1 ) )

proof end;

consistency
for b₁ being Supergraph of G1 holds verum ;

end;

:: deftheorem Def26 defines GraphUnion GLIB_014:def 26 :
for G1, G2 being _Graph
for b₃ being Supergraph of G1 holds
( ( G1 tolerates G2 implies ( b₃ is GraphUnion of G1,G2 iff ex S being GraphUnionSet st
( S = {G1,G2} & b₃ is GraphUnion of S ) ) ) & ( not G1 tolerates G2 implies ( b₃ is GraphUnion of G1,G2 iff b₃ == G1 ) ) );

:: not really needed
::definition
::let G1, G2 be _Graph;
::func G1 \/ G2 equals the plain GraphUnion of G1, G2;
::end;

theorem Th25: :: GLIB_014:25

for G1, G2, G being _Graph st G1 tolerates G2 holds
( G is GraphUnion of G1,G2 iff ( the_Vertices_of G = (the_Vertices_of G1) \/ (the_Vertices_of G2) & the_Edges_of G = (the_Edges_of G1) \/ (the_Edges_of G2) & the_Source_of G = (the_Source_of G1) +* (the_Source_of G2) & the_Target_of G = (the_Target_of G1) +* (the_Target_of G2) ) )

proof end;

theorem Th26: :: GLIB_014:26

for G1, G2 being _Graph
for G being GraphUnion of G1,G2 st G1 tolerates G2 holds
G is Supergraph of G2

proof end;

theorem :: GLIB_014:27

for G1, G2 being _Graph
for G being GraphUnion of G1,G2 st G1 tolerates G2 holds
G is GraphUnion of G2,G1

proof end;

theorem Th28: :: GLIB_014:28

for G1, G2, G9 being _Graph
for G being GraphUnion of G1,G2 holds
( G9 is GraphUnion of G1,G2 iff G == G9 )

proof end;

registration

let G1, G2 be _Graph;

cluster Relation-like NAT -defined Function-like finite [Graph-like] plain for GraphUnion of G1,G2;

existence
ex b₁ being GraphUnion of G1,G2 st b₁ is plain

proof end;

end;

theorem :: GLIB_014:29

for G, G1 being _Graph
for G2 being Subgraph of G1 holds
( G is GraphUnion of G1,G2 iff G == G1 )

proof end;

registration

let G1, G2 be loopless _Graph;

cluster -> loopless for GraphUnion of G1,G2;

coherence
for b₁ being GraphUnion of G1,G2 holds b₁ is loopless

proof end;

end;

registration

let G1, G2 be edgeless _Graph;

cluster -> edgeless for GraphUnion of G1,G2;

coherence
for b₁ being GraphUnion of G1,G2 holds b₁ is edgeless

proof end;

end;

registration

let G1, G2 be loopfull _Graph;

cluster -> loopfull for GraphUnion of G1,G2;

coherence
for b₁ being GraphUnion of G1,G2 holds b₁ is loopfull

proof end;

end;

theorem Th30: :: GLIB_014:30

for G1 being _Graph
for G2 being DLGraphComplement of G1
for G being GraphUnion of G1,G2
for v, w being Vertex of G ex e being object st e DJoins v,w,G

proof end;

registration

let G1 be _Graph;
let G2 be DLGraphComplement of G1;

cluster -> complete loopfull for GraphUnion of G1,G2;

coherence
for b₁ being GraphUnion of G1,G2 holds
( b₁ is loopfull & b₁ is complete )

proof end;

end;

theorem Th31: :: GLIB_014:31

for G1 being _Graph
for G2 being LGraphComplement of G1
for G being GraphUnion of G1,G2
for v, w being Vertex of G ex e being object st e Joins v,w,G

proof end;

registration

let G1 be _Graph;
let G2 be LGraphComplement of G1;

cluster -> complete loopfull for GraphUnion of G1,G2;

coherence
for b₁ being GraphUnion of G1,G2 holds
( b₁ is loopfull & b₁ is complete )

proof end;

end;

theorem Th32: :: GLIB_014:32

for G1 being _Graph
for G2 being DGraphComplement of G1
for G being GraphUnion of G1,G2
for v, w being Vertex of G st v <> w holds
ex e being object st e DJoins v,w,G

proof end;

registration

let G1 be _Graph;
let G2 be DGraphComplement of G1;

cluster -> complete for GraphUnion of G1,G2;

coherence
for b₁ being GraphUnion of G1,G2 holds b₁ is complete

proof end;

end;

theorem Th33: :: GLIB_014:33

for G1 being _Graph
for G2 being GraphComplement of G1
for G being GraphUnion of G1,G2
for v, w being Vertex of G st v <> w holds
ex e being object st e Joins v,w,G

proof end;

registration

let G1 be _Graph;
let G2 be GraphComplement of G1;

cluster -> complete for GraphUnion of G1,G2;

coherence
for b₁ being GraphUnion of G1,G2 holds b₁ is complete

proof end;

end;

registration

let G1 be non-Dmulti _Graph;
let G2 be DLGraphComplement of G1;

cluster -> non-Dmulti for GraphUnion of G1,G2;

coherence
for b₁ being GraphUnion of G1,G2 holds b₁ is non-Dmulti

proof end;

end;

registration

let G1 be non-multi _Graph;
let G2 be LGraphComplement of G1;

cluster -> non-multi for GraphUnion of G1,G2;

coherence
for b₁ being GraphUnion of G1,G2 holds b₁ is non-multi

proof end;

end;

registration

let G1 be non-Dmulti _Graph;
let G2 be DGraphComplement of G1;

cluster -> non-Dmulti for GraphUnion of G1,G2;

coherence
for b₁ being GraphUnion of G1,G2 holds b₁ is non-Dmulti

proof end;

end;

registration

let G1 be non-multi _Graph;
let G2 be GraphComplement of G1;

cluster -> non-multi for GraphUnion of G1,G2;

coherence
for b₁ being GraphUnion of G1,G2 holds b₁ is non-multi

proof end;

end;

definition

let S be Graph-membered set ;

attr S is /\-tolerating means :Def27: :: GLIB_014:def 27
( meet (the_Vertices_of S) <> {} & ( for G1, G2 being _Graph st G1 in S & G2 in S holds
G1 tolerates G2 ) );

end;

:: deftheorem Def27 defines /\-tolerating GLIB_014:def 27 :
for S being Graph-membered set holds
( S is /\-tolerating iff ( meet (the_Vertices_of S) <> {} & ( for G1, G2 being _Graph st G1 in S & G2 in S holds
G1 tolerates G2 ) ) );

definition

let S be non empty Graph-membered set ;

redefine attr S is /\-tolerating means :: GLIB_014:def 28
( meet (the_Vertices_of S) <> {} & ( for G1, G2 being Element of S holds G1 tolerates G2 ) );

compatibility
( S is /\-tolerating iff ( meet (the_Vertices_of S) <> {} & ( for G1, G2 being Element of S holds G1 tolerates G2 ) ) ) ;

end;

:: deftheorem defines /\-tolerating GLIB_014:def 28 :
for S being non empty Graph-membered set holds
( S is /\-tolerating iff ( meet (the_Vertices_of S) <> {} & ( for G1, G2 being Element of S holds G1 tolerates G2 ) ) );

theorem Th34: :: GLIB_014:34

for S being Graph-membered set holds
( S is /\-tolerating iff ( S is \/-tolerating & meet (the_Vertices_of S) <> {} ) ) ;

registration

let G be _Graph;

cluster {G} -> /\-tolerating ;

coherence
{G} is /\-tolerating

proof end;

end;

registration

cluster Graph-membered /\-tolerating -> non empty Graph-membered \/-tolerating for set ;

coherence
for b₁ being Graph-membered set st b₁ is /\-tolerating holds
( b₁ is \/-tolerating & not b₁ is empty )

proof end;

cluster Graph-membered /\-tolerating for set ;

existence
ex b₁ being Graph-membered set st b₁ is /\-tolerating

proof end;

end;

definition

mode GraphMeetSet is Graph-membered /\-tolerating set ;

end;

registration

let S be GraphMeetSet;

cluster meet (the_Vertices_of S) -> non empty ;

coherence
not meet (the_Vertices_of S) is empty by Def27;

end;

theorem Th35: :: GLIB_014:35

for G1, G2 being _Graph holds
( ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 ) iff {G1,G2} is /\-tolerating )

proof end;

theorem :: GLIB_014:36

for S1, S2 being non empty Graph-membered set st S1 \/ S2 is /\-tolerating holds
( S1 is /\-tolerating & S2 is /\-tolerating )

proof end;

registration

let S be GraphMeetSet;

cluster meet (the_Source_of S) -> Relation-like Function-like ;

coherence
( meet (the_Source_of S) is Function-like & meet (the_Source_of S) is Relation-like ) ;

cluster meet (the_Target_of S) -> Relation-like Function-like ;

coherence
( meet (the_Target_of S) is Function-like & meet (the_Target_of S) is Relation-like ) ;

end;

registration

let S be GraphMeetSet;

cluster meet (the_Source_of S) -> meet (the_Edges_of S) -defined meet (the_Vertices_of S) -valued ;

coherence
( meet (the_Source_of S) is meet (the_Edges_of S) -defined & meet (the_Source_of S) is meet (the_Vertices_of S) -valued )

proof end;

cluster meet (the_Target_of S) -> meet (the_Edges_of S) -defined meet (the_Vertices_of S) -valued ;

coherence
( meet (the_Target_of S) is meet (the_Edges_of S) -defined & meet (the_Target_of S) is meet (the_Vertices_of S) -valued )

proof end;

end;

registration

let S be GraphMeetSet;

cluster meet (the_Source_of S) -> total ;

coherence
meet (the_Source_of S) is total

proof end;

cluster meet (the_Target_of S) -> total ;

coherence
meet (the_Target_of S) is total

proof end;

end;

:: a.k.a. Graph Intersection, but not to be confused with Intersection Graph

definition

let S be GraphMeetSet;

mode GraphMeet of S -> _Graph means :Def29: :: GLIB_014:def 29
( the_Vertices_of it = meet (the_Vertices_of S) & the_Edges_of it = meet (the_Edges_of S) & the_Source_of it = meet (the_Source_of S) & the_Target_of it = meet (the_Target_of S) );

existence
ex b₁ being _Graph st
( the_Vertices_of b₁ = meet (the_Vertices_of S) & the_Edges_of b₁ = meet (the_Edges_of S) & the_Source_of b₁ = meet (the_Source_of S) & the_Target_of b₁ = meet (the_Target_of S) )

proof end;

end;

:: deftheorem Def29 defines GraphMeet GLIB_014:def 29 :
for S being GraphMeetSet
for b₂ being _Graph holds
( b₂ is GraphMeet of S iff ( the_Vertices_of b₂ = meet (the_Vertices_of S) & the_Edges_of b₂ = meet (the_Edges_of S) & the_Source_of b₂ = meet (the_Source_of S) & the_Target_of b₂ = meet (the_Target_of S) ) );

:: not really needed
::definition
::let S be GraphMeetSet;
::func meet S equals the plain GraphMeet of S;
::end;
:: not proven here (DOM from CARD_3)
:: theorem
:: for S being GraphMeetSet, G being GraphMeet of S
:: holds DOM(the_Source_of S) = dom the_Source_of G &
:: DOM(the_Target_of S) = dom the_Target_of G;

theorem Th37: :: GLIB_014:37

for S being GraphMeetSet
for G being GraphMeet of S
for H being Element of S holds H is Supergraph of G

proof end;

theorem Th38: :: GLIB_014:38

for S being GraphMeetSet
for G being GraphMeet of S
for G9 being _Graph holds
( G9 is GraphMeet of S iff G == G9 )

proof end;

registration

let S be GraphMeetSet;

cluster Relation-like NAT -defined Function-like finite [Graph-like] plain for GraphMeet of S;

existence
ex b₁ being GraphMeet of S st b₁ is plain

proof end;

end;

theorem :: GLIB_014:39

for G, H being _Graph holds
( G is GraphMeet of {H} iff G == H )

proof end;

definition

let G1, G2 be _Graph;

mode GraphMeet of G1,G2 -> Subgraph of G1 means :Def30: :: GLIB_014:def 30
ex S being GraphMeetSet st
( S = {G1,G2} & it is GraphMeet of S ) if ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 )
otherwise it == G1;

existence
( ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 implies ex b₁ being Subgraph of G1 ex S being GraphMeetSet st
( S = {G1,G2} & b₁ is GraphMeet of S ) ) & ( ( not G1 tolerates G2 or not the_Vertices_of G1 meets the_Vertices_of G2 ) implies ex b₁ being Subgraph of G1 st b₁ == G1 ) )

proof end;

consistency
for b₁ being Subgraph of G1 holds verum ;

end;

:: deftheorem Def30 defines GraphMeet GLIB_014:def 30 :
for G1, G2 being _Graph
for b₃ being Subgraph of G1 holds
( ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 implies ( b₃ is GraphMeet of G1,G2 iff ex S being GraphMeetSet st
( S = {G1,G2} & b₃ is GraphMeet of S ) ) ) & ( ( not G1 tolerates G2 or not the_Vertices_of G1 meets the_Vertices_of G2 ) implies ( b₃ is GraphMeet of G1,G2 iff b₃ == G1 ) ) );

:: not really needed
::definition
::let G1, G2 be _Graph;
::func G1 /\ G2 equals the plain GraphMeet of G1, G2;
::end;

theorem Th40: :: GLIB_014:40

for G1, G2, G being _Graph st G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 holds
( G is GraphMeet of G1,G2 iff ( the_Vertices_of G = (the_Vertices_of G1) /\ (the_Vertices_of G2) & the_Edges_of G = (the_Edges_of G1) /\ (the_Edges_of G2) & the_Source_of G = (the_Source_of G1) /\ (the_Source_of G2) & the_Target_of G = (the_Target_of G1) /\ (the_Target_of G2) ) )

proof end;

theorem Th41: :: GLIB_014:41

for G1, G2 being _Graph
for G being GraphMeet of G1,G2 st G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 holds
G is Subgraph of G2

proof end;

theorem :: GLIB_014:42

for G1, G2 being _Graph
for G being GraphMeet of G1,G2 st G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 holds
G is GraphMeet of G2,G1

proof end;

theorem Th43: :: GLIB_014:43

for G1, G2, G9 being _Graph
for G being GraphMeet of G1,G2 holds
( G9 is GraphMeet of G1,G2 iff G == G9 )

proof end;

registration

let G1, G2 be _Graph;

cluster Relation-like NAT -defined Function-like finite [Graph-like] plain for GraphMeet of G1,G2;

existence
ex b₁ being GraphMeet of G1,G2 st b₁ is plain

proof end;

end;

theorem :: GLIB_014:44

for G, G1 being _Graph
for G2 being Subgraph of G1 holds
( G is GraphMeet of G1,G2 iff G == G2 )

proof end;

theorem Th45: :: GLIB_014:45

for G1, G2 being _Graph
for G being GraphMeet of G1,G2 st the_Vertices_of G1 meets the_Vertices_of G2 & the_Edges_of G1 misses the_Edges_of G2 holds
G is edgeless

proof end;

registration

let G1 be _Graph;
let G2 be DLGraphComplement of G1;

cluster -> edgeless for GraphMeet of G1,G2;

coherence
for b₁ being GraphMeet of G1,G2 holds b₁ is edgeless

proof end;

end;

registration

let G1 be _Graph;
let G2 be LGraphComplement of G1;

cluster -> edgeless for GraphMeet of G1,G2;

coherence
for b₁ being GraphMeet of G1,G2 holds b₁ is edgeless

proof end;

end;

registration

let G1 be _Graph;
let G2 be DGraphComplement of G1;

cluster -> edgeless for GraphMeet of G1,G2;

coherence
for b₁ being GraphMeet of G1,G2 holds b₁ is edgeless

proof end;

end;

registration

let G1 be _Graph;
let G2 be GraphComplement of G1;

cluster -> edgeless for GraphMeet of G1,G2;

coherence
for b₁ being GraphMeet of G1,G2 holds b₁ is edgeless

proof end;

end;