:: About Graph Unions and Intersections
:: by Sebastian Koch
::
:: Received May 19, 2020
:: Copyright (c) 2020-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 NUMBERS, FINSET_1, RELAT_1, FUNCT_1, XBOOLE_0, TARSKI, SUBSET_1,
FUNCT_4, ZFMISC_1, CARD_1, GLIB_000, GLIB_002, PARTFUN1, CHORD, SCMYCIEL,
REWRITE1, GLIB_006, GLIB_007, GLIB_009, GLIB_012, RELAT_2, GLIB_014,
SETFAM_1, TREES_1, MSUALG_6;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, SETFAM_1, FUNCT_4, FINSET_1, CARD_1, NUMBERS, COMPUT_1,
GLIB_000, GLIB_002, CHORD, GLIB_006, GLIB_007, GLIB_008, GLIB_009,
GLIBPRE0, GLIB_012;
constructors FUNCT_4, RELSET_1, CHORD, GLIB_002, GLIB_007, GLIB_008, GLIB_009,
GLIB_012, COMPUT_1, GLIBPRE0;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, CARD_1, RELSET_1,
GLIB_000, GLIB_002, GLIB_009, GLIB_008, GLIB_012, COMPUT_1, GLIBPRE0;
requirements BOOLE, SUBSET;
begin :: Sets of Graphs
definition
let X be set;
attr X is Graph-membered means
:: GLIB_014:def 1
for x being object st x in X holds x is _Graph;
end;
registration
cluster empty -> Graph-membered for set;
end;
registration
let F be Graph-yielding Function;
cluster rng F -> Graph-membered;
end;
registration
let G1 be _Graph;
cluster {G1} -> Graph-membered;
let G2 be _Graph;
cluster {G1, G2} -> Graph-membered;
end;
:: there is no functor/mode yet
:: to construct an infinite number of graphs at once
registration
cluster empty Graph-membered for set;
cluster trivial finite non empty Graph-membered for set;
end;
registration
let X be Graph-membered set;
cluster -> Graph-membered for Subset of X;
end;
:: the usual set operations preserve graph membership
registration
let X be Graph-membered set, Y be set;
cluster X /\ Y -> Graph-membered;
cluster X \ Y -> Graph-membered;
end;
registration
let X, Y be Graph-membered set;
cluster X \/ Y -> Graph-membered;
cluster X \+\ Y -> 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;
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;
registration
let X be non empty Graph-membered set;
cluster -> Function-like Relation-like for Element of X;
end;
registration
let X be non empty Graph-membered set;
cluster -> NAT-defined finite for Element of X;
end;
registration
let X be non empty Graph-membered set;
cluster -> [Graph-like] for Element of X;
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
:: GLIB_014:def 2
for G being _Graph st G in S holds G is plain;
attr S is loopless means
:: GLIB_014:def 3
for G being _Graph st G in S holds G is loopless;
attr S is non-multi means
:: GLIB_014:def 4
for G being _Graph st G in S holds G is non-multi;
attr S is non-Dmulti means
:: 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
:: GLIB_014:def 8
for G being _Graph st G in S holds G is acyclic;
attr S is connected means
:: 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
:: GLIB_014:def 11
for G being _Graph st G in S holds G is chordal;
attr S is edgeless means
:: GLIB_014:def 12
for G being _Graph st G in S holds G is edgeless;
attr S is loopfull means
:: GLIB_014:def 13
for G being _Graph st G in S holds G is loopfull;
::attr S is vertex-finite means
::for G being _Graph st G in S holds G is vertex-finite;
::attr S is edge-finite means
::for G being _Graph st G in S holds G is edge-finite;
end;
:: negative clustering are omitted, because
:: negative attributes (e.g. "non-loopless") are not defined yet
registration
cluster empty -> plain loopless non-multi non-Dmulti simple Dsimple
acyclic connected Tree-like chordal edgeless loopfull
:: vertex-finite edge-finite;
for Graph-membered set;
cluster non-multi -> non-Dmulti for Graph-membered set;
cluster loopless non-multi -> simple for Graph-membered set;
cluster loopless non-Dmulti -> Dsimple for Graph-membered set;
cluster simple -> loopless non-multi for Graph-membered set;
cluster Dsimple -> loopless non-Dmulti for Graph-membered set;
cluster acyclic -> simple for Graph-membered set;
cluster acyclic connected -> Tree-like for Graph-membered set;
cluster Tree-like -> acyclic connected for Graph-membered set;
end;
registration
let G1 be plain _Graph;
cluster {G1} -> plain;
let G2 be plain _Graph;
cluster {G1, G2} -> plain;
end;
registration
let G1 be loopless _Graph;
cluster {G1} -> loopless;
let G2 be loopless _Graph;
cluster {G1, G2} -> loopless;
end;
registration
let G1 be non-multi _Graph;
cluster {G1} -> non-multi;
let G2 be non-multi _Graph;
cluster {G1, G2} -> non-multi;
end;
registration
let G1 be non-Dmulti _Graph;
cluster {G1} -> non-Dmulti;
let G2 be non-Dmulti _Graph;
cluster {G1, G2} -> non-Dmulti;
end;
registration
let G1 be simple _Graph;
cluster {G1} -> simple;
let G2 be simple _Graph;
cluster {G1, G2} -> simple;
end;
registration
let G1 be Dsimple _Graph;
cluster {G1} -> Dsimple;
let G2 be Dsimple _Graph;
cluster {G1, G2} -> Dsimple;
end;
registration
let G1 be acyclic _Graph;
cluster {G1} -> acyclic;
let G2 be acyclic _Graph;
cluster {G1, G2} -> acyclic;
end;
registration
let G1 be connected _Graph;
cluster {G1} -> connected;
let G2 be connected _Graph;
cluster {G1, G2} -> connected;
end;
registration
let G1 be Tree-like _Graph;
cluster {G1} -> Tree-like;
let G2 be Tree-like _Graph;
cluster {G1, G2} -> Tree-like;
end;
registration
let G1 be chordal _Graph;
cluster {G1} -> chordal;
let G2 be chordal _Graph;
cluster {G1, G2} -> chordal;
end;
registration
let G1 be edgeless _Graph;
cluster {G1} -> edgeless;
let G2 be edgeless _Graph;
cluster {G1, G2} -> edgeless;
end;
registration
let G1 be loopfull _Graph;
cluster {G1} -> loopfull;
let G2 be loopfull _Graph;
cluster {G1, G2} -> loopfull;
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 :: GLIB_014:3
for F being Graph-yielding Function holds
(F is plain iff rng F is plain) &
(F is loopless iff rng F is loopless) &
(F is non-multi iff rng F is non-multi) &
(F is non-Dmulti iff rng F is non-Dmulti) &
(F is acyclic iff rng F is acyclic) &
(F is connected iff rng F is connected) &
(F is chordal iff rng F is chordal) &
(F is edgeless iff rng F is edgeless) &
(F is loopfull iff rng F is loopfull);
theorem :: GLIB_014:4
for F being Graph-yielding Function holds
(F is simple iff rng F is simple) &
(F is Dsimple iff rng F is Dsimple) &
(F is Tree-like iff rng F is Tree-like);
registration
let F be plain Graph-yielding Function;
cluster rng F -> plain;
end;
registration
let F be loopless Graph-yielding Function;
cluster rng F -> loopless;
end;
registration
let F be non-multi Graph-yielding Function;
cluster rng F -> non-multi;
end;
registration
let F be non-Dmulti Graph-yielding Function;
cluster rng F -> non-Dmulti;
end;
registration
let F be simple Graph-yielding Function;
cluster rng F -> simple;
end;
registration
let F be Dsimple Graph-yielding Function;
cluster rng F -> Dsimple;
end;
registration
let F be acyclic Graph-yielding Function;
cluster rng F -> acyclic;
end;
registration
let F be connected Graph-yielding Function;
cluster rng F -> connected;
end;
registration
let F be Tree-like Graph-yielding Function;
cluster rng F -> Tree-like;
end;
registration
let F be chordal Graph-yielding Function;
cluster rng F -> chordal;
end;
registration
let F be edgeless Graph-yielding Function;
cluster rng F -> edgeless;
end;
registration
let F be loopfull Graph-yielding Function;
cluster rng F -> loopfull;
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 plain Graph-membered set;
cluster -> plain for Subset of X;
end;
registration
let X be loopless Graph-membered set;
cluster -> loopless for Subset of X;
end;
registration
let X be non-multi Graph-membered set;
cluster -> non-multi for Subset of X;
end;
registration
let X be non-Dmulti Graph-membered set;
cluster -> non-Dmulti for Subset of X;
end;
registration
let X be simple Graph-membered set;
cluster -> simple for Subset of X;
end;
registration
let X be Dsimple Graph-membered set;
cluster -> Dsimple for Subset of X;
end;
registration
let X be acyclic Graph-membered set;
cluster -> acyclic for Subset of X;
end;
registration
let X be connected Graph-membered set;
cluster -> connected for Subset of X;
end;
registration
let X be Tree-like Graph-membered set;
cluster -> Tree-like for Subset of X;
end;
registration
let X be chordal Graph-membered set;
cluster -> chordal for Subset of X;
end;
registration
let X be edgeless Graph-membered set;
cluster -> edgeless for Subset of X;
end;
registration
let X be loopfull Graph-membered set;
cluster -> loopfull for Subset of X;
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 plain Graph-membered set, Y be set;
cluster X /\ Y -> plain;
cluster X \ Y -> plain;
end;
registration
let X, Y be plain Graph-membered set;
cluster X \/ Y -> plain;
cluster X \+\ Y -> plain;
end;
registration
let X be loopless Graph-membered set, Y be set;
cluster X /\ Y -> loopless;
cluster X \ Y -> loopless;
end;
registration
let X, Y be loopless Graph-membered set;
cluster X \/ Y -> loopless;
cluster X \+\ Y -> loopless;
end;
registration
let X be non-multi Graph-membered set, Y be set;
cluster X /\ Y -> non-multi;
cluster X \ Y -> non-multi;
end;
registration
let X, Y be non-multi Graph-membered set;
cluster X \/ Y -> non-multi;
cluster X \+\ Y -> non-multi;
end;
registration
let X be non-Dmulti Graph-membered set, Y be set;
cluster X /\ Y -> non-Dmulti;
cluster X \ Y -> non-Dmulti;
end;
registration
let X, Y be non-Dmulti Graph-membered set;
cluster X \/ Y -> non-Dmulti;
cluster X \+\ Y -> non-Dmulti;
end;
registration
let X be simple Graph-membered set, Y be set;
cluster X /\ Y -> simple;
cluster X \ Y -> simple;
end;
registration
let X, Y be simple Graph-membered set;
cluster X \/ Y -> simple;
cluster X \+\ Y -> simple;
end;
registration
let X be Dsimple Graph-membered set, Y be set;
cluster X /\ Y -> Dsimple;
cluster X \ Y -> Dsimple;
end;
registration
let X, Y be Dsimple Graph-membered set;
cluster X \/ Y -> Dsimple;
cluster X \+\ Y -> Dsimple;
end;
registration
let X be acyclic Graph-membered set, Y be set;
cluster X /\ Y -> acyclic;
cluster X \ Y -> acyclic;
end;
registration
let X, Y be acyclic Graph-membered set;
cluster X \/ Y -> acyclic;
cluster X \+\ Y -> acyclic;
end;
registration
let X be connected Graph-membered set, Y be set;
cluster X /\ Y -> connected;
cluster X \ Y -> connected;
end;
registration
let X, Y be connected Graph-membered set;
cluster X \/ Y -> connected;
cluster X \+\ Y -> connected;
end;
registration
let X be Tree-like Graph-membered set, Y be set;
cluster X /\ Y -> Tree-like;
cluster X \ Y -> Tree-like;
end;
registration
let X, Y be Tree-like Graph-membered set;
cluster X \/ Y -> Tree-like;
cluster X \+\ Y -> Tree-like;
end;
registration
let X be chordal Graph-membered set, Y be set;
cluster X /\ Y -> chordal;
cluster X \ Y -> chordal;
end;
registration
let X, Y be chordal Graph-membered set;
cluster X \/ Y -> chordal;
cluster X \+\ Y -> chordal;
end;
registration
let X be edgeless Graph-membered set, Y be set;
cluster X /\ Y -> edgeless;
cluster X \ Y -> edgeless;
end;
registration
let X, Y be edgeless Graph-membered set;
cluster X \/ Y -> edgeless;
cluster X \+\ Y -> edgeless;
end;
registration
let X be loopfull Graph-membered set, Y be set;
cluster X /\ Y -> loopfull;
cluster X \ Y -> loopfull;
end;
registration
let X, Y be loopfull Graph-membered set;
cluster X \/ Y -> loopfull;
cluster X \+\ Y -> 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 plain loopless non-multi non-Dmulti simple Dsimple
acyclic connected Tree-like chordal edgeless loopfull
for Graph-membered set;
cluster non empty Tree-like acyclic connected simple Dsimple loopless
non-multi non-Dmulti for Graph-membered set;
cluster non empty edgeless chordal for Graph-membered set;
cluster non empty loopfull for Graph-membered set;
cluster non empty plain for Graph-membered set;
::cluster non empty vertex-finite edge-finite for Graph-membered set;
::existence;
end;
registration
let S be non empty plain Graph-membered set;
cluster -> plain for Element of S;
end;
registration
let S be non empty loopless Graph-membered set;
cluster -> loopless for Element of S;
end;
registration
let S be non empty non-multi Graph-membered set;
cluster -> non-multi for Element of S;
end;
registration
let S be non empty non-Dmulti Graph-membered set;
cluster -> non-Dmulti for Element of S;
end;
registration
let S be non empty simple Graph-membered set;
cluster -> simple for Element of S;
end;
registration
let S be non empty Dsimple Graph-membered set;
cluster -> Dsimple for Element of S;
end;
registration
let S be non empty acyclic Graph-membered set;
cluster -> acyclic for Element of S;
end;
registration
let S be non empty connected Graph-membered set;
cluster -> connected for Element of S;
end;
registration
let S be non empty Tree-like Graph-membered set;
cluster -> Tree-like for Element of S;
end;
registration
let S be non empty chordal Graph-membered set;
cluster -> chordal for Element of S;
end;
registration
let S be non empty edgeless Graph-membered set;
cluster -> edgeless for Element of S;
end;
registration
let S be non empty loopfull Graph-membered set;
cluster -> loopfull for Element of S;
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
:: 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;
func the_Edges_of S -> set means
:: 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;
func the_Source_of S -> set means
:: 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;
func the_Target_of S -> set means
:: 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;
end;
definition
let S be non empty Graph-membered set;
redefine func the_Vertices_of S equals
:: GLIB_014:def 18
the set of all the_Vertices_of G where G is Element of S;
redefine func the_Edges_of S equals
:: GLIB_014:def 19
the set of all the_Edges_of G where G is Element of S;
redefine func the_Source_of S equals
:: GLIB_014:def 20
the set of all the_Source_of G where G is Element of S;
redefine func the_Target_of S equals
:: GLIB_014:def 21
the set of all the_Target_of G where G is Element of S;
end;
registration
let S be non empty Graph-membered set;
cluster union the_Vertices_of S -> non empty;
end;
registration
let S be Graph-membered set;
cluster the_Source_of S -> functional;
cluster the_Target_of S -> functional;
end;
registration
let S be empty Graph-membered set;
cluster the_Vertices_of S -> empty;
cluster the_Edges_of S -> empty;
cluster the_Source_of S -> empty;
cluster the_Target_of S -> empty;
end;
registration
let S be non empty Graph-membered set;
cluster the_Vertices_of S -> non empty;
cluster the_Edges_of S -> non empty;
cluster the_Source_of S -> non empty;
cluster the_Target_of S -> non empty;
end;
registration
let S be trivial Graph-membered set;
cluster the_Vertices_of S -> trivial;
cluster the_Edges_of S -> trivial;
cluster the_Source_of S -> trivial;
cluster the_Target_of S -> trivial;
end;
theorem :: 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};
theorem :: 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};
theorem :: 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;
registration
let S be finite Graph-membered set;
cluster the_Vertices_of S -> finite;
cluster the_Edges_of S -> finite;
cluster the_Source_of S -> finite;
cluster the_Target_of S -> finite;
end;
registration
let S be edgeless Graph-membered set;
cluster union the_Edges_of S -> empty;
end;
theorem :: 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;
:: 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;
theorem :: 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);
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);
begin :: Union of Graphs
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;
symmetry;
end;
theorem :: GLIB_014:12
for G1, G2 being _Graph st the_Edges_of G1 misses the_Edges_of G2
holds G1 tolerates G2;
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;
theorem :: GLIB_014:14
for G1 being _Graph, G2, G3 being Subgraph of G1 holds G2 tolerates G3;
theorem :: GLIB_014:15
for G1 being _Graph, G2 being Subgraph of G1 holds G1 tolerates G2;
theorem :: GLIB_014:16
for G1, G2 being _Graph st G1 == G2 holds G1 tolerates G2;
theorem :: 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;
theorem :: GLIB_014:18
for G1 being _Graph, E being Subset of the_Edges_of G1
for G2 being reverseEdgeDirections of G1, E
holds G1 tolerates G2 iff E c= G1.loops();
definition
let S be Graph-membered set;
attr S is \/-tolerating means
:: GLIB_014:def 23
for G1, G2 being _Graph st G1 in S & G2 in S holds G1 tolerates G2;
end;
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;
end;
registration
cluster empty -> \/-tolerating for Graph-membered set;
let G be _Graph;
cluster {G} -> \/-tolerating;
end;
registration
cluster non empty \/-tolerating for Graph-membered set;
end;
definition
mode GraphUnionSet is non empty \/-tolerating Graph-membered set;
end;
theorem :: GLIB_014:19
for G1, G2 being _Graph holds G1 tolerates G2 iff {G1,G2} is \/-tolerating;
registration
let S1 be \/-tolerating Graph-membered set, S2 be set;
cluster S1 /\ S2 -> \/-tolerating;
cluster S1 \ S2 -> \/-tolerating;
end;
theorem :: GLIB_014:20
for S1, S2 being Graph-membered set st S1 \/ S2 is \/-tolerating
holds S1 is \/-tolerating & S2 is \/-tolerating;
registration
let S be \/-tolerating Graph-membered set;
cluster the_Source_of S -> compatible;
cluster the_Target_of S -> compatible;
end;
registration
let S be \/-tolerating Graph-membered set;
cluster union the_Source_of S -> Function-like Relation-like;
cluster union the_Target_of S -> Function-like Relation-like;
end;
registration
let S be \/-tolerating Graph-membered set;
cluster union the_Source_of S -> (union the_Edges_of S)-defined
(union the_Vertices_of S)-valued;
cluster union the_Target_of S -> (union the_Edges_of S)-defined
(union the_Vertices_of S)-valued;
end;
registration
let S be \/-tolerating Graph-membered set;
cluster union the_Source_of S -> total;
cluster union the_Target_of S -> total;
end;
definition
let S be GraphUnionSet;
mode GraphUnion of S -> _Graph means
:: 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;
end;
:: 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 :: GLIB_014:21
for S being GraphUnionSet, G being GraphUnion of S, H being Element of S
holds H is Subgraph of G;
theorem :: GLIB_014:22
for S being GraphUnionSet, G being GraphUnion of S, G9 being _Graph
holds G9 is GraphUnion of S iff G == G9;
registration
let S be GraphUnionSet;
cluster plain for GraphUnion of S;
end;
registration
cluster loopless for GraphUnionSet;
cluster edgeless for GraphUnionSet;
cluster loopfull for GraphUnionSet;
end;
theorem :: GLIB_014:23
for S being GraphUnionSet, G being GraphUnion of S holds
(S is loopless iff G is loopless) &
(S is edgeless iff G is edgeless) &
(S is loopfull implies G is loopfull);
registration
let S be loopless GraphUnionSet;
cluster -> loopless for GraphUnion of S;
end;
registration
let S be edgeless GraphUnionSet;
cluster -> edgeless for GraphUnion of S;
end;
registration
let S be loopfull GraphUnionSet;
cluster -> loopfull for GraphUnion of S;
end;
theorem :: GLIB_014:24
for G, H being _Graph holds G is GraphUnion of {H} iff G == H;
definition
let G1, G2 be _Graph;
mode GraphUnion of G1, G2 -> Supergraph of G1 means
:: GLIB_014:def 26
ex S being GraphUnionSet st S = {G1,G2} & it is GraphUnion of S
if G1 tolerates G2
otherwise it == G1;
end;
:: not really needed
::definition
::let G1, G2 be _Graph;
::func G1 \/ G2 equals the plain GraphUnion of G1, G2;
::end;
theorem :: 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;
theorem :: GLIB_014:26
for G1, G2 being _Graph, G being GraphUnion of G1, G2
st G1 tolerates G2 holds G is Supergraph of G2;
theorem :: GLIB_014:27
for G1, G2 being _Graph, G being GraphUnion of G1, G2
st G1 tolerates G2 holds G is GraphUnion of G2, G1;
theorem :: GLIB_014:28
for G1, G2, G9 being _Graph, G being GraphUnion of G1, G2
holds G9 is GraphUnion of G1, G2 iff G == G9;
registration
let G1, G2 be _Graph;
cluster plain for GraphUnion of G1, G2;
end;
theorem :: GLIB_014:29
for G, G1 being _Graph, G2 being Subgraph of G1
holds G is GraphUnion of G1, G2 iff G == G1;
registration
let G1, G2 be loopless _Graph;
cluster -> loopless for GraphUnion of G1, G2;
end;
registration
let G1, G2 be edgeless _Graph;
cluster -> edgeless for GraphUnion of G1, G2;
end;
registration
let G1, G2 be loopfull _Graph;
cluster -> loopfull for GraphUnion of G1, G2;
end;
theorem :: GLIB_014:30
for G1 being _Graph, G2 being DLGraphComplement of G1
for G being GraphUnion of G1, G2, v, w being Vertex of G
ex e being object st e DJoins v,w,G;
registration
let G1 be _Graph, G2 be DLGraphComplement of G1;
cluster -> loopfull complete for GraphUnion of G1, G2;
end;
theorem :: GLIB_014:31
for G1 being _Graph, G2 being LGraphComplement of G1
for G being GraphUnion of G1, G2, v, w being Vertex of G
ex e being object st e Joins v,w,G;
registration
let G1 be _Graph, G2 be LGraphComplement of G1;
cluster -> loopfull complete for GraphUnion of G1, G2;
end;
theorem :: GLIB_014:32
for G1 being _Graph, G2 being DGraphComplement of G1
for G being GraphUnion of G1, G2, v, w being Vertex of G
st v <> w ex e being object st e DJoins v,w,G;
registration
let G1 be _Graph, G2 be DGraphComplement of G1;
cluster -> complete for GraphUnion of G1, G2;
end;
theorem :: GLIB_014:33
for G1 being _Graph, G2 being GraphComplement of G1
for G being GraphUnion of G1, G2, v, w being Vertex of G
st v <> w ex e being object st e Joins v,w,G;
registration
let G1 be _Graph, G2 be GraphComplement of G1;
cluster -> complete for GraphUnion of G1, G2;
end;
registration
let G1 be non-Dmulti _Graph, G2 be DLGraphComplement of G1;
cluster -> non-Dmulti for GraphUnion of G1, G2;
end;
registration
let G1 be non-multi _Graph, G2 be LGraphComplement of G1;
cluster -> non-multi for GraphUnion of G1, G2;
end;
registration
let G1 be non-Dmulti _Graph, G2 be DGraphComplement of G1;
cluster -> non-Dmulti for GraphUnion of G1, G2;
end;
registration
let G1 be non-multi _Graph, G2 be GraphComplement of G1;
cluster -> non-multi for GraphUnion of G1, G2;
end;
begin :: Meet of Graphs
definition
let S be Graph-membered set;
attr S is /\-tolerating means
:: 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;
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;
end;
theorem :: 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;
end;
registration
cluster /\-tolerating -> \/-tolerating non empty for Graph-membered set;
cluster /\-tolerating for Graph-membered set;
end;
definition
mode GraphMeetSet is /\-tolerating Graph-membered set;
end;
registration
let S be GraphMeetSet;
cluster meet the_Vertices_of S -> non empty;
end;
theorem :: 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;
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;
registration
let S be GraphMeetSet;
cluster meet the_Source_of S -> Function-like Relation-like;
cluster meet the_Target_of S -> Function-like 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;
cluster meet the_Target_of S -> (meet the_Edges_of S)-defined
(meet the_Vertices_of S)-valued;
end;
registration
let S be GraphMeetSet;
cluster meet the_Source_of S -> total;
cluster meet the_Target_of S -> total;
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
:: 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;
end;
:: 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 :: GLIB_014:37
for S being GraphMeetSet, G being GraphMeet of S, H being Element of S
holds H is Supergraph of G;
theorem :: GLIB_014:38
for S being GraphMeetSet, G being GraphMeet of S, G9 being _Graph
holds G9 is GraphMeet of S iff G == G9;
registration
let S be GraphMeetSet;
cluster plain for GraphMeet of S;
end;
theorem :: GLIB_014:39
for G, H being _Graph holds G is GraphMeet of {H} iff G == H;
definition
let G1, G2 be _Graph;
mode GraphMeet of G1, G2 -> Subgraph of G1 means
:: 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;
end;
:: not really needed
::definition
::let G1, G2 be _Graph;
::func G1 /\ G2 equals the plain GraphMeet of G1, G2;
::end;
theorem :: 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;
theorem :: GLIB_014:41
for G1, G2 being _Graph, 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;
theorem :: GLIB_014:42
for G1, G2 being _Graph, 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;
theorem :: GLIB_014:43
for G1, G2, G9 being _Graph, G being GraphMeet of G1, G2
holds G9 is GraphMeet of G1, G2 iff G == G9;
registration
let G1, G2 be _Graph;
cluster plain for GraphMeet of G1, G2;
end;
theorem :: GLIB_014:44
for G, G1 being _Graph, G2 being Subgraph of G1
holds G is GraphMeet of G1, G2 iff G == G2;
theorem :: GLIB_014:45
for G1, G2 being _Graph, 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;
registration
let G1 be _Graph, G2 be DLGraphComplement of G1;
cluster -> edgeless for GraphMeet of G1, G2;
end;
registration
let G1 be _Graph, G2 be LGraphComplement of G1;
cluster -> edgeless for GraphMeet of G1, G2;
end;
registration
let G1 be _Graph, G2 be DGraphComplement of G1;
cluster -> edgeless for GraphMeet of G1, G2;
end;
registration
let G1 be _Graph, G2 be GraphComplement of G1;
cluster -> edgeless for GraphMeet of G1, G2;
end;