:: Graphs of Functions
:: by Czes{\l}aw Byli\'nski
::
:: Received April 14, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users

theorem Th1: :: GRFUNC_1:1

for f being Function
for G being set st G c= f holds
G is Function ;

theorem Th2: :: GRFUNC_1:2

for f, g being Function holds
( f c= g iff ( dom f c= dom g & ( for x being object st x in dom f holds
f . x = g . x ) ) )

proof end;

theorem :: GRFUNC_1:3

for f, g being Function st dom f = dom g & f c= g holds
f = g

proof end;

Lm1: for x, y being object
for f, h being Function st (rng f) /\ (rng h) = {} & x in dom f & y in dom h holds
f . x <> h . y

proof end;

theorem :: GRFUNC_1:4

for x, z being object
for f, g being Function st [x,z] in g * f holds
( [x,(f . x)] in f & [(f . x),z] in g )

proof end;

theorem :: GRFUNC_1:5

for x, y being object holds {[x,y]} is Function ;

Lm2: for x, x1, y, y1 being object st [x,y] in {[x1,y1]} holds
( x = x1 & y = y1 )

proof end;

theorem :: GRFUNC_1:6

for x, y being object
for f being Function st f = {[x,y]} holds
f . x = y

proof end;

theorem Th7: :: GRFUNC_1:7

for x being object
for f being Function st dom f = {x} holds
f = {[x,(f . x)]}

proof end;

theorem :: GRFUNC_1:8

for x1, x2, y1, y2 being object holds
( {[x1,y1],[x2,y2]} is Function iff ( x1 = x2 implies y1 = y2 ) )

proof end;

theorem Th9: :: GRFUNC_1:9

for f being Function holds
( f is one-to-one iff for x1, x2, y being object st [x1,y] in f & [x2,y] in f holds
x1 = x2 )

proof end;

theorem Th10: :: GRFUNC_1:10

for f, g being Function st g c= f & f is one-to-one holds
g is one-to-one

proof end;

registration

let f be Function;
let X be set ;

cluster f /\ X -> Function-like ;

coherence
f /\ X is Function-like by Th1, XBOOLE_1:17;

end;

theorem :: GRFUNC_1:11

for x being object
for f, g being Function st x in dom (f /\ g) holds
(f /\ g) . x = f . x

proof end;

theorem :: GRFUNC_1:12

for f, g being Function st f is one-to-one holds
f /\ g is one-to-one by Th10, XBOOLE_1:17;

theorem :: GRFUNC_1:13

for f, g being Function st dom f misses dom g holds
f \/ g is Function

proof end;

theorem :: GRFUNC_1:14

for f, g, h being Function st f c= h & g c= h holds
f \/ g is Function by Th1, XBOOLE_1:8;

Lm3: for x being object
for f, g, h being Function st h = f \/ g holds
( x in dom h iff ( x in dom f or x in dom g ) )

proof end;

theorem Th15: :: GRFUNC_1:15

for x being object
for f, g, h being Function st x in dom g & h = f \/ g holds
h . x = g . x

proof end;

theorem :: GRFUNC_1:16

for x being object
for f, g, h being Function st x in dom h & h = f \/ g & not h . x = f . x holds
h . x = g . x

proof end;

theorem :: GRFUNC_1:17

for f, g, h being Function st f is one-to-one & g is one-to-one & h = f \/ g & rng f misses rng g holds
h is one-to-one

proof end;

theorem :: GRFUNC_1:18

canceled;

theorem :: GRFUNC_1:19

canceled;

::$CT 2

theorem :: GRFUNC_1:20

for f being Function st f is one-to-one holds
for x, y being object holds
( [y,x] in f " iff [x,y] in f )

proof end;

theorem :: GRFUNC_1:21

for f being Function st f = {} holds
f " = {}

proof end;

theorem :: GRFUNC_1:22

for X being set
for x being object
for f being Function holds
( ( x in dom f & x in X ) iff [x,(f . x)] in f | X )

proof end;

theorem Th21: :: GRFUNC_1:23

for f, g being Function st g c= f holds
f | (dom g) = g

proof end;

theorem :: GRFUNC_1:24

for Y being set
for x being object
for f being Function holds
( ( x in dom f & f . x in Y ) iff [x,(f . x)] in Y |` f )

proof end;

theorem :: GRFUNC_1:25

for f, g being Function st g c= f & f is one-to-one holds
(rng g) |` f = g

proof end;

theorem :: GRFUNC_1:26

for Y being set
for x being object
for f being Function holds
( x in f " Y iff ( [x,(f . x)] in f & f . x in Y ) )

proof end;

:: from HAHNBAN

theorem :: GRFUNC_1:27

for X being set
for f, g being Function st X c= dom f & f c= g holds
f | X = g | X

proof end;

:: from AMI_3

theorem Th26: :: GRFUNC_1:28

for f being Function
for x being set st x in dom f holds
f | {x} = {[x,(f . x)]}

proof end;

:: from AMI_3, 2007.06.14, A.T.

theorem Th27: :: GRFUNC_1:29

for f, g being Function
for x being set st dom f = dom g & f . x = g . x holds
f | {x} = g | {x}

proof end;

theorem Th28: :: GRFUNC_1:30

for f, g being Function
for x, y being set st dom f = dom g & f . x = g . x & f . y = g . y holds
f | {x,y} = g | {x,y}

proof end;

theorem :: GRFUNC_1:31

for f, g being Function
for x, y, z being set st dom f = dom g & f . x = g . x & f . y = g . y & f . z = g . z holds
f | {x,y,z} = g | {x,y,z}

proof end;

:: from AMISTD_2, 2007.07.26, A.T.

registration

let f be Function;
let A be set ;

cluster f \ A -> Function-like ;

coherence
f \ A is Function-like ;

end;

theorem :: GRFUNC_1:32

for x being object
for f, g being Function st x in (dom f) \ (dom g) holds
(f \ g) . x = f . x

proof end;

:: missing, 2007.06.19, A.T.

theorem :: GRFUNC_1:33

for f, g, h being Function st f c= g & f c= h holds
g | (dom f) = h | (dom f)

proof end;

:: new, 2009.09.30, A.T.

registration

let f be Function;
let g be Subset of f;

cluster Relation-like Function-like g -compatible -> f -compatible for set ;

coherence
for b₁ being Function st b₁ is g -compatible holds
b₁ is f -compatible

proof end;

end;

:: 2009.10.17, A.T.

theorem Th32: :: GRFUNC_1:34

for f, g being Function st g c= f holds
g = f | (dom g)

proof end;

registration

let f be Function;
let g be f -compatible Function;

cluster -> f -compatible for Element of K10(g);

coherence
for b₁ being Subset of g holds b₁ is f -compatible

proof end;

end;

theorem :: GRFUNC_1:35

for X being set
for x being object
for f, g being Function st g c= f & x in X & X /\ (dom f) c= dom g holds
f . x = g . x

proof end;