:: by Masami Tanaka and Yatsuka Nakamura

::

:: Received January 26, 2004

:: Copyright (c) 2004-2021 Association of Mizar Users

definition

let T be non empty RelStr ;

let A be Subset of T;

{ x where x is Element of T : for y being Element of T st y in A ` holds

not x in U_FT y } is Subset of T

end;
let A be Subset of T;

func A ^d -> Subset of T equals :: FINTOPO3:def 1

{ x where x is Element of T : for y being Element of T st y in A ` holds

not x in U_FT y } ;

coherence { x where x is Element of T : for y being Element of T st y in A ` holds

not x in U_FT y } ;

{ x where x is Element of T : for y being Element of T st y in A ` holds

not x in U_FT y } is Subset of T

proof end;

:: deftheorem defines ^d FINTOPO3:def 1 :

for T being non empty RelStr

for A being Subset of T holds A ^d = { x where x is Element of T : for y being Element of T st y in A ` holds

not x in U_FT y } ;

for T being non empty RelStr

for A being Subset of T holds A ^d = { x where x is Element of T : for y being Element of T st y in A ` holds

not x in U_FT y } ;

theorem Th2: :: FINTOPO3:2

for T being non empty RelStr

for A being Subset of T

for x being Element of T holds

( x in A ^d iff for y being Element of T st y in A ` holds

not x in U_FT y )

for A being Subset of T

for x being Element of T holds

( x in A ^d iff for y being Element of T st y in A ` holds

not x in U_FT y )

proof end;

definition

let T be non empty RelStr ;

let A be Subset of T;

ex b_{1} being sequence of (bool the carrier of T) st

( ( for n being Nat

for B being Subset of T st B = b_{1} . n holds

b_{1} . (n + 1) = B ^b ) & b_{1} . 0 = A )

for b_{1}, b_{2} being sequence of (bool the carrier of T) st ( for n being Nat

for B being Subset of T st B = b_{1} . n holds

b_{1} . (n + 1) = B ^b ) & b_{1} . 0 = A & ( for n being Nat

for B being Subset of T st B = b_{2} . n holds

b_{2} . (n + 1) = B ^b ) & b_{2} . 0 = A holds

b_{1} = b_{2}

end;
let A be Subset of T;

func Fcl A -> sequence of (bool the carrier of T) means :Def2: :: FINTOPO3:def 2

( ( for n being Nat

for B being Subset of T st B = it . n holds

it . (n + 1) = B ^b ) & it . 0 = A );

existence ( ( for n being Nat

for B being Subset of T st B = it . n holds

it . (n + 1) = B ^b ) & it . 0 = A );

ex b

( ( for n being Nat

for B being Subset of T st B = b

b

proof end;

uniqueness for b

for B being Subset of T st B = b

b

for B being Subset of T st B = b

b

b

proof end;

:: deftheorem Def2 defines Fcl FINTOPO3:def 2 :

for T being non empty RelStr

for A being Subset of T

for b_{3} being sequence of (bool the carrier of T) holds

( b_{3} = Fcl A iff ( ( for n being Nat

for B being Subset of T st B = b_{3} . n holds

b_{3} . (n + 1) = B ^b ) & b_{3} . 0 = A ) );

for T being non empty RelStr

for A being Subset of T

for b

( b

for B being Subset of T st B = b

b

definition

let T be non empty RelStr ;

let A be Subset of T;

let n be Nat;

coherence

(Fcl A) . n is Subset of T

end;
let A be Subset of T;

let n be Nat;

coherence

(Fcl A) . n is Subset of T

proof end;

:: deftheorem defines Fcl FINTOPO3:def 3 :

for T being non empty RelStr

for A being Subset of T

for n being Nat holds Fcl (A,n) = (Fcl A) . n;

for T being non empty RelStr

for A being Subset of T

for n being Nat holds Fcl (A,n) = (Fcl A) . n;

definition

let T be non empty RelStr ;

let A be Subset of T;

ex b_{1} being sequence of (bool the carrier of T) st

( ( for n being Nat

for B being Subset of T st B = b_{1} . n holds

b_{1} . (n + 1) = B ^i ) & b_{1} . 0 = A )

for b_{1}, b_{2} being sequence of (bool the carrier of T) st ( for n being Nat

for B being Subset of T st B = b_{1} . n holds

b_{1} . (n + 1) = B ^i ) & b_{1} . 0 = A & ( for n being Nat

for B being Subset of T st B = b_{2} . n holds

b_{2} . (n + 1) = B ^i ) & b_{2} . 0 = A holds

b_{1} = b_{2}

end;
let A be Subset of T;

func Fint A -> sequence of (bool the carrier of T) means :Def4: :: FINTOPO3:def 4

( ( for n being Nat

for B being Subset of T st B = it . n holds

it . (n + 1) = B ^i ) & it . 0 = A );

existence ( ( for n being Nat

for B being Subset of T st B = it . n holds

it . (n + 1) = B ^i ) & it . 0 = A );

ex b

( ( for n being Nat

for B being Subset of T st B = b

b

proof end;

uniqueness for b

for B being Subset of T st B = b

b

for B being Subset of T st B = b

b

b

proof end;

:: deftheorem Def4 defines Fint FINTOPO3:def 4 :

for T being non empty RelStr

for A being Subset of T

for b_{3} being sequence of (bool the carrier of T) holds

( b_{3} = Fint A iff ( ( for n being Nat

for B being Subset of T st B = b_{3} . n holds

b_{3} . (n + 1) = B ^i ) & b_{3} . 0 = A ) );

for T being non empty RelStr

for A being Subset of T

for b

( b

for B being Subset of T st B = b

b

definition

let T be non empty RelStr ;

let A be Subset of T;

let n be Nat;

coherence

(Fint A) . n is Subset of T

end;
let A be Subset of T;

let n be Nat;

coherence

(Fint A) . n is Subset of T

proof end;

:: deftheorem defines Fint FINTOPO3:def 5 :

for T being non empty RelStr

for A being Subset of T

for n being Nat holds Fint (A,n) = (Fint A) . n;

for T being non empty RelStr

for A being Subset of T

for n being Nat holds Fint (A,n) = (Fint A) . n;

theorem :: FINTOPO3:13

theorem :: FINTOPO3:14

theorem Th17: :: FINTOPO3:17

for T being non empty RelStr

for A, B being Subset of T

for n being Nat holds Fcl ((A \/ B),n) = (Fcl (A,n)) \/ (Fcl (B,n))

for A, B being Subset of T

for n being Nat holds Fcl ((A \/ B),n) = (Fcl (A,n)) \/ (Fcl (B,n))

proof end;

theorem :: FINTOPO3:18

theorem :: FINTOPO3:19

theorem Th22: :: FINTOPO3:22

for T being non empty RelStr

for A, B being Subset of T

for n being Nat holds Fint ((A /\ B),n) = (Fint (A,n)) /\ (Fint (B,n))

for A, B being Subset of T

for n being Nat holds Fint ((A /\ B),n) = (Fint (A,n)) /\ (Fint (B,n))

proof end;

theorem :: FINTOPO3:23

for T being non empty RelStr

for A being Subset of T st T is filled holds

for n being Nat holds A c= Fcl (A,n)

for A being Subset of T st T is filled holds

for n being Nat holds A c= Fcl (A,n)

proof end;

theorem :: FINTOPO3:24

for T being non empty RelStr

for A being Subset of T st T is filled holds

for n being Nat holds Fint (A,n) c= A

for A being Subset of T st T is filled holds

for n being Nat holds Fint (A,n) c= A

proof end;

theorem :: FINTOPO3:25

for T being non empty RelStr

for A being Subset of T st T is filled holds

for n being Nat holds Fcl (A,n) c= Fcl (A,(n + 1))

for A being Subset of T st T is filled holds

for n being Nat holds Fcl (A,n) c= Fcl (A,(n + 1))

proof end;

theorem :: FINTOPO3:26

for T being non empty RelStr

for A being Subset of T st T is filled holds

for n being Nat holds Fint (A,(n + 1)) c= Fint (A,n)

for A being Subset of T st T is filled holds

for n being Nat holds Fint (A,(n + 1)) c= Fint (A,n)

proof end;

theorem Th27: :: FINTOPO3:27

for T being non empty RelStr

for A being Subset of T

for n being Nat holds (Fint ((A `),n)) ` = Fcl (A,n)

for A being Subset of T

for n being Nat holds (Fint ((A `),n)) ` = Fcl (A,n)

proof end;

theorem Th28: :: FINTOPO3:28

for T being non empty RelStr

for A being Subset of T

for n being Nat holds (Fcl ((A `),n)) ` = Fint (A,n)

for A being Subset of T

for n being Nat holds (Fcl ((A `),n)) ` = Fint (A,n)

proof end;

theorem :: FINTOPO3:29

for T being non empty RelStr

for A, B being Subset of T

for n being Nat holds (Fcl (A,n)) \/ (Fcl (B,n)) = (Fint (((A \/ B) `),n)) `

for A, B being Subset of T

for n being Nat holds (Fcl (A,n)) \/ (Fcl (B,n)) = (Fint (((A \/ B) `),n)) `

proof end;

theorem :: FINTOPO3:30

for T being non empty RelStr

for A, B being Subset of T

for n being Nat holds (Fint (A,n)) /\ (Fint (B,n)) = (Fcl (((A /\ B) `),n)) `

for A, B being Subset of T

for n being Nat holds (Fint (A,n)) /\ (Fint (B,n)) = (Fcl (((A /\ B) `),n)) `

proof end;

:: Function of Inflation Series

definition

let T be non empty RelStr ;

let A be Subset of T;

ex b_{1} being sequence of (bool the carrier of T) st

( ( for n being Nat

for B being Subset of T st B = b_{1} . n holds

b_{1} . (n + 1) = B ^f ) & b_{1} . 0 = A )

for b_{1}, b_{2} being sequence of (bool the carrier of T) st ( for n being Nat

for B being Subset of T st B = b_{1} . n holds

b_{1} . (n + 1) = B ^f ) & b_{1} . 0 = A & ( for n being Nat

for B being Subset of T st B = b_{2} . n holds

b_{2} . (n + 1) = B ^f ) & b_{2} . 0 = A holds

b_{1} = b_{2}

end;
let A be Subset of T;

func Finf A -> sequence of (bool the carrier of T) means :Def6: :: FINTOPO3:def 6

( ( for n being Nat

for B being Subset of T st B = it . n holds

it . (n + 1) = B ^f ) & it . 0 = A );

existence ( ( for n being Nat

for B being Subset of T st B = it . n holds

it . (n + 1) = B ^f ) & it . 0 = A );

ex b

( ( for n being Nat

for B being Subset of T st B = b

b

proof end;

uniqueness for b

for B being Subset of T st B = b

b

for B being Subset of T st B = b

b

b

proof end;

:: deftheorem Def6 defines Finf FINTOPO3:def 6 :

for T being non empty RelStr

for A being Subset of T

for b_{3} being sequence of (bool the carrier of T) holds

( b_{3} = Finf A iff ( ( for n being Nat

for B being Subset of T st B = b_{3} . n holds

b_{3} . (n + 1) = B ^f ) & b_{3} . 0 = A ) );

for T being non empty RelStr

for A being Subset of T

for b

( b

for B being Subset of T st B = b

b

definition

let T be non empty RelStr ;

let A be Subset of T;

let n be Nat;

coherence

(Finf A) . n is Subset of T

end;
let A be Subset of T;

let n be Nat;

coherence

(Finf A) . n is Subset of T

proof end;

:: deftheorem defines Finf FINTOPO3:def 7 :

for T being non empty RelStr

for A being Subset of T

for n being Nat holds Finf (A,n) = (Finf A) . n;

for T being non empty RelStr

for A being Subset of T

for n being Nat holds Finf (A,n) = (Finf A) . n;

:: Function of Deflation Series

definition

let T be non empty RelStr ;

let A be Subset of T;

ex b_{1} being sequence of (bool the carrier of T) st

( ( for n being Nat

for B being Subset of T st B = b_{1} . n holds

b_{1} . (n + 1) = B ^d ) & b_{1} . 0 = A )

for b_{1}, b_{2} being sequence of (bool the carrier of T) st ( for n being Nat

for B being Subset of T st B = b_{1} . n holds

b_{1} . (n + 1) = B ^d ) & b_{1} . 0 = A & ( for n being Nat

for B being Subset of T st B = b_{2} . n holds

b_{2} . (n + 1) = B ^d ) & b_{2} . 0 = A holds

b_{1} = b_{2}

end;
let A be Subset of T;

func Fdfl A -> sequence of (bool the carrier of T) means :Def8: :: FINTOPO3:def 8

( ( for n being Nat

for B being Subset of T st B = it . n holds

it . (n + 1) = B ^d ) & it . 0 = A );

existence ( ( for n being Nat

for B being Subset of T st B = it . n holds

it . (n + 1) = B ^d ) & it . 0 = A );

ex b

( ( for n being Nat

for B being Subset of T st B = b

b

proof end;

uniqueness for b

for B being Subset of T st B = b

b

for B being Subset of T st B = b

b

b

proof end;

:: deftheorem Def8 defines Fdfl FINTOPO3:def 8 :

for T being non empty RelStr

for A being Subset of T

for b_{3} being sequence of (bool the carrier of T) holds

( b_{3} = Fdfl A iff ( ( for n being Nat

for B being Subset of T st B = b_{3} . n holds

b_{3} . (n + 1) = B ^d ) & b_{3} . 0 = A ) );

for T being non empty RelStr

for A being Subset of T

for b

( b

for B being Subset of T st B = b

b

definition

let T be non empty RelStr ;

let A be Subset of T;

let n be Nat;

coherence

(Fdfl A) . n is Subset of T

end;
let A be Subset of T;

let n be Nat;

coherence

(Fdfl A) . n is Subset of T

proof end;

:: deftheorem defines Fdfl FINTOPO3:def 9 :

for T being non empty RelStr

for A being Subset of T

for n being Nat holds Fdfl (A,n) = (Fdfl A) . n;

for T being non empty RelStr

for A being Subset of T

for n being Nat holds Fdfl (A,n) = (Fdfl A) . n;

theorem :: FINTOPO3:31

theorem :: FINTOPO3:32

theorem :: FINTOPO3:35

for T being non empty RelStr

for A, B being Subset of T

for n being Nat holds Finf ((A \/ B),n) = (Finf (A,n)) \/ (Finf (B,n))

for A, B being Subset of T

for n being Nat holds Finf ((A \/ B),n) = (Finf (A,n)) \/ (Finf (B,n))

proof end;

theorem :: FINTOPO3:36

for T being non empty RelStr

for A being Subset of T st T is filled holds

for n being Nat holds A c= Finf (A,n)

for A being Subset of T st T is filled holds

for n being Nat holds A c= Finf (A,n)

proof end;

theorem :: FINTOPO3:37

for T being non empty RelStr

for A being Subset of T st T is filled holds

for n being Nat holds Finf (A,n) c= Finf (A,(n + 1))

for A being Subset of T st T is filled holds

for n being Nat holds Finf (A,n) c= Finf (A,(n + 1))

proof end;

theorem :: FINTOPO3:38

theorem :: FINTOPO3:39

theorem Th42: :: FINTOPO3:42

for T being non empty RelStr

for A, B being Subset of T

for n being Nat holds Fdfl ((A /\ B),n) = (Fdfl (A,n)) /\ (Fdfl (B,n))

for A, B being Subset of T

for n being Nat holds Fdfl ((A /\ B),n) = (Fdfl (A,n)) /\ (Fdfl (B,n))

proof end;

theorem :: FINTOPO3:43

for T being non empty RelStr

for A being Subset of T st T is filled holds

for n being Nat holds Fdfl (A,n) c= A

for A being Subset of T st T is filled holds

for n being Nat holds Fdfl (A,n) c= A

proof end;

theorem :: FINTOPO3:44

for T being non empty RelStr

for A being Subset of T st T is filled holds

for n being Nat holds Fdfl (A,(n + 1)) c= Fdfl (A,n)

for A being Subset of T st T is filled holds

for n being Nat holds Fdfl (A,(n + 1)) c= Fdfl (A,n)

proof end;

theorem Th45: :: FINTOPO3:45

for T being non empty RelStr

for A being Subset of T

for n being Nat holds Fdfl (A,n) = (Finf ((A `),n)) `

for A being Subset of T

for n being Nat holds Fdfl (A,n) = (Finf ((A `),n)) `

proof end;

theorem :: FINTOPO3:46

for T being non empty RelStr

for A, B being Subset of T

for n being Nat holds (Fdfl (A,n)) /\ (Fdfl (B,n)) = (Finf (((A /\ B) `),n)) `

for A, B being Subset of T

for n being Nat holds (Fdfl (A,n)) /\ (Fdfl (B,n)) = (Finf (((A /\ B) `),n)) `

proof end;

definition

let T be non empty RelStr ;

let n be Nat;

let x be Element of T;

coherence

Finf ((U_FT x),n) is Subset of T ;

end;
let n be Nat;

let x be Element of T;

coherence

Finf ((U_FT x),n) is Subset of T ;

:: deftheorem defines U_FT FINTOPO3:def 10 :

for T being non empty RelStr

for n being Nat

for x being Element of T holds U_FT (x,n) = Finf ((U_FT x),n);

for T being non empty RelStr

for n being Nat

for x being Element of T holds U_FT (x,n) = Finf ((U_FT x),n);

theorem :: FINTOPO3:47

theorem :: FINTOPO3:48

definition

let S, T be non empty RelStr ;

for S, T being non empty RelStr st the carrier of S = the carrier of T & ( for x being Element of S

for y being Element of T holds

( y in U_FT x iff x in U_FT y ) ) holds

( the carrier of T = the carrier of S & ( for x being Element of T

for y being Element of S holds

( y in U_FT x iff x in U_FT y ) ) ) ;

end;
pred S,T are_mutually_symmetric means :: FINTOPO3:def 11

( the carrier of S = the carrier of T & ( for x being Element of S

for y being Element of T holds

( y in U_FT x iff x in U_FT y ) ) );

symmetry ( the carrier of S = the carrier of T & ( for x being Element of S

for y being Element of T holds

( y in U_FT x iff x in U_FT y ) ) );

for S, T being non empty RelStr st the carrier of S = the carrier of T & ( for x being Element of S

for y being Element of T holds

( y in U_FT x iff x in U_FT y ) ) holds

( the carrier of T = the carrier of S & ( for x being Element of T

for y being Element of S holds

( y in U_FT x iff x in U_FT y ) ) ) ;

:: deftheorem defines are_mutually_symmetric FINTOPO3:def 11 :

for S, T being non empty RelStr holds

( S,T are_mutually_symmetric iff ( the carrier of S = the carrier of T & ( for x being Element of S

for y being Element of T holds

( y in U_FT x iff x in U_FT y ) ) ) );

for S, T being non empty RelStr holds

( S,T are_mutually_symmetric iff ( the carrier of S = the carrier of T & ( for x being Element of S

for y being Element of T holds

( y in U_FT x iff x in U_FT y ) ) ) );

:: (A^f is an inflation of A).