:: YELLOW14 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem :: YELLOW14:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
bool 1 = {0,1} by CARD_5:1, ZFMISC_1:30;

theorem Th2: :: YELLOW14:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for Y being Subset of X holds rng ((id X) | Y) = Y
proof end;

theorem Th3: :: YELLOW14:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function
for a, b being set holds (f +* (a .--> b)) . a = b
proof end;

registration
cluster empty strict RelStr ;
existence
ex b1 being RelStr st
( b1 is strict & b1 is empty )
proof end;
end;

theorem Th4: :: YELLOW14:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being empty 1-sorted
for T being 1-sorted
for f being Function of S,T st rng f = [#] T holds
T is empty
proof end;

theorem Th5: :: YELLOW14:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being 1-sorted
for T being empty 1-sorted
for f being Function of S,T st dom f = [#] S holds
S is empty
proof end;

theorem :: YELLOW14:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty 1-sorted
for T being 1-sorted
for f being Function of S,T st dom f = [#] S holds
not T is empty
proof end;

theorem :: YELLOW14:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being 1-sorted
for T being non empty 1-sorted
for f being Function of S,T st rng f = [#] T holds
not S is empty
proof end;

definition
let S be non empty reflexive RelStr ;
let T be non empty RelStr ;
let f be Function of S,T;
redefine attr f is directed-sups-preserving means :: YELLOW14:def 1
for X being non empty directed Subset of S holds f preserves_sup_of X;
compatibility
( f is directed-sups-preserving iff for X being non empty directed Subset of S holds f preserves_sup_of X )
proof end;
end;

:: deftheorem defines directed-sups-preserving YELLOW14:def 1 :
for S being non empty reflexive RelStr
for T being non empty RelStr
for f being Function of S,T holds
( f is directed-sups-preserving iff for X being non empty directed Subset of S holds f preserves_sup_of X );

definition
let R be 1-sorted ;
let N be NetStr of R;
attr N is Function-yielding means :Def2: :: YELLOW14:def 2
the mapping of N is Function-yielding;
end;

:: deftheorem Def2 defines Function-yielding YELLOW14:def 2 :
for R being 1-sorted
for N being NetStr of R holds
( N is Function-yielding iff the mapping of N is Function-yielding );

registration
cluster strict non empty constituted-Functions 1-sorted ;
existence
ex b1 being 1-sorted st
( b1 is strict & not b1 is empty & b1 is constituted-Functions )
proof end;
end;

registration
cluster non empty strict constituted-Functions RelStr ;
existence
ex b1 being RelStr st
( b1 is strict & not b1 is empty & b1 is constituted-Functions )
proof end;
end;

registration
let R be constituted-Functions 1-sorted ;
cluster -> Function-yielding NetStr of R;
coherence
for b1 being NetStr of R holds b1 is Function-yielding
proof end;
end;

registration
let R be constituted-Functions 1-sorted ;
cluster strict Function-yielding NetStr of R;
existence
ex b1 being NetStr of R st
( b1 is strict & b1 is Function-yielding )
proof end;
end;

registration
let R be non empty constituted-Functions 1-sorted ;
cluster non empty strict Function-yielding NetStr of R;
existence
ex b1 being NetStr of R st
( b1 is strict & not b1 is empty & b1 is Function-yielding )
proof end;
end;

registration
let R be constituted-Functions 1-sorted ;
let N be Function-yielding NetStr of R;
cluster the mapping of N -> Function-yielding ;
coherence
the mapping of N is Function-yielding by Def2;
end;

registration
let R be non empty constituted-Functions 1-sorted ;
cluster strict Function-yielding NetStr of R;
existence
ex b1 being net of R st
( b1 is strict & b1 is Function-yielding )
proof end;
end;

registration
let S be non empty 1-sorted ;
let N be non empty NetStr of S;
cluster rng the mapping of N -> non empty ;
coherence
not rng the mapping of N is empty ;
end;

registration
let S be non empty 1-sorted ;
let N be non empty NetStr of S;
cluster rng (netmap N,S) -> non empty ;
coherence
not rng (netmap N,S) is empty ;
end;

theorem :: YELLOW14:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being non empty RelStr
for f being Function of B,C
for g, h being Function of A,B st g <= h & f is monotone holds
f * g <= f * h
proof end;

theorem :: YELLOW14:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty TopSpace
for T being non empty TopSpace-like TopRelStr
for f, g being Function of S,T
for x, y being Element of (ContMaps S,T) st x = f & y = g holds
( x <= y iff f <= g )
proof end;

definition
let I be non empty set ;
let R be non empty RelStr ;
let f be Element of (R |^ I);
let i be Element of I;
:: original: .
redefine func f . i -> Element of R;
coherence
f . i is Element of R
proof end;
end;

theorem Th10: :: YELLOW14:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being RelStr
for f being Function of S,T st f is isomorphic holds
f is onto
proof end;

registration
let S, T be RelStr ;
cluster isomorphic -> onto Relation of the carrier of S,the carrier of T;
coherence
for b1 being Function of S,T st b1 is isomorphic holds
b1 is onto by Th10;
end;

theorem Th11: :: YELLOW14:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty RelStr
for f being Function of S,T st f is isomorphic holds
f /" is isomorphic
proof end;

theorem :: YELLOW14:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty RelStr st S,T are_isomorphic & S is with_infima holds
T is with_infima
proof end;

theorem :: YELLOW14:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty RelStr st S,T are_isomorphic & S is with_suprema holds
T is with_suprema
proof end;

theorem Th14: :: YELLOW14:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being RelStr st L is empty holds
L is bounded
proof end;

registration
cluster empty -> bounded RelStr ;
coherence
for b1 being RelStr st b1 is empty holds
b1 is bounded by Th14;
end;

theorem :: YELLOW14:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being RelStr st S,T are_isomorphic & S is lower-bounded holds
T is lower-bounded
proof end;

theorem :: YELLOW14:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being RelStr st S,T are_isomorphic & S is upper-bounded holds
T is upper-bounded
proof end;

theorem :: YELLOW14:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty RelStr
for A being Subset of S
for f being Function of S,T st f is isomorphic & ex_sup_of A,S holds
ex_sup_of f .: A,T
proof end;

theorem :: YELLOW14:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty RelStr
for A being Subset of S
for f being Function of S,T st f is isomorphic & ex_inf_of A,S holds
ex_inf_of f .: A,T
proof end;

theorem :: YELLOW14:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being TopStruct st ( S,T are_homeomorphic or ex f being Function of S,T st
( dom f = [#] S & rng f = [#] T ) ) holds
( S is empty iff T is empty )
proof end;

theorem :: YELLOW14:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace holds T, TopStruct(# the carrier of T,the topology of T #) are_homeomorphic
proof end;

registration
let T be non empty reflexive Scott TopRelStr ;
cluster open -> upper inaccessible Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is open holds
( b1 is inaccessible_by_directed_joins & b1 is upper ) by WAYBEL11:def 4;
cluster upper inaccessible -> open Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is inaccessible_by_directed_joins & b1 is upper holds
b1 is open by WAYBEL11:def 4;
end;

theorem :: YELLOW14:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopStruct
for x, y being Point of T
for X, Y being Subset of T st X = {x} & Cl X c= Cl Y holds
x in Cl Y
proof end;

theorem :: YELLOW14:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopStruct
for x, y being Point of T
for Y, V being Subset of T st Y = {y} & x in Cl Y & V is open & x in V holds
y in V
proof end;

theorem :: YELLOW14:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopStruct
for x, y being Point of T
for X, Y being Subset of T st X = {x} & Y = {y} & ( for V being Subset of T st V is open & x in V holds
y in V ) holds
Cl X c= Cl Y
proof end;

theorem Th24: :: YELLOW14:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty TopSpace
for A being irreducible Subset of S
for B being Subset of T st A = B & TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) holds
B is irreducible
proof end;

theorem Th25: :: YELLOW14:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty TopSpace
for a being Point of S
for b being Point of T
for A being Subset of S
for B being Subset of T st a = b & A = B & TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) & a is_dense_point_of A holds
b is_dense_point_of B
proof end;

theorem Th26: :: YELLOW14:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being TopStruct
for A being Subset of S
for B being Subset of T st A = B & TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) & A is compact holds
B is compact
proof end;

theorem :: YELLOW14:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty TopSpace st TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) & S is sober holds
T is sober
proof end;

theorem :: YELLOW14:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty TopSpace st TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) & S is locally-compact holds
T is locally-compact
proof end;

theorem :: YELLOW14:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being TopStruct st TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) & S is compact holds
T is compact
proof end;

definition
let I be non empty set ;
let T be non empty TopSpace;
let x be Point of (product (I --> T));
let i be Element of I;
:: original: .
redefine func x . i -> Element of T;
coherence
x . i is Element of T
proof end;
end;

theorem Th30: :: YELLOW14:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of M
for x, y being Point of (product J) holds
( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} )
proof end;

theorem :: YELLOW14:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty set
for T being non empty TopSpace
for x, y being Point of (product (M --> T)) holds
( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} )
proof end;

theorem Th32: :: YELLOW14:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty set
for i being Element of M
for J being non-Empty TopSpace-yielding ManySortedSet of M
for x being Point of (product J) holds pi (Cl {x}),i = Cl {(x . i)}
proof end;

theorem :: YELLOW14:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty set
for i being Element of M
for T being non empty TopSpace
for x being Point of (product (M --> T)) holds pi (Cl {x}),i = Cl {(x . i)}
proof end;

theorem :: YELLOW14:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopStruct
for f being Function of X,Y
for g being Function of Y,X st f = id X & g = id X & f is continuous & g is continuous holds
TopStruct(# the carrier of X,the topology of X #) = TopStruct(# the carrier of Y,the topology of Y #)
proof end;

theorem :: YELLOW14:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for f being Function of X,Y st corestr f is continuous holds
f is continuous
proof end;

registration
let X be non empty TopSpace;
let Y be non empty SubSpace of X;
cluster incl Y -> continuous ;
coherence
incl Y is continuous by TMAP_1:98;
end;

theorem :: YELLOW14:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for f being Function of T,T st f * f = f holds
(corestr f) * (incl (Image f)) = id (Image f)
proof end;

theorem :: YELLOW14:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty TopSpace
for W being non empty SubSpace of Y holds corestr (incl W) is_homeomorphism
proof end;

theorem Th38: :: YELLOW14:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of M st ( for i being Element of M holds J . i is T_0 TopSpace ) holds
product J is T_0
proof end;

registration
let I be non empty set ;
let T be non empty T_0 TopSpace;
cluster product (I --> T) -> T_0 ;
coherence
product (I --> T) is T_0
proof end;
end;

theorem Th39: :: YELLOW14:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of M st ( for i being Element of M holds
( J . i is being_T1 & J . i is TopSpace-like ) ) holds
product J is_T1
proof end;

registration
let I be non empty set ;
let T be non empty being_T1 TopSpace;
cluster product (I --> T) -> being_T1 ;
coherence
product (I --> T) is being_T1
proof end;
end;