:: by Bart{\l}omiej Skorulski

::

:: Received May 23, 2000

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

theorem Th1: :: YELLOW17:1

for F being Function

for i, xi being set

for Ai being Subset of (F . i) st (proj (F,i)) " {xi} meets (proj (F,i)) " Ai holds

xi in Ai

for i, xi being set

for Ai being Subset of (F . i) st (proj (F,i)) " {xi} meets (proj (F,i)) " Ai holds

xi in Ai

proof end;

theorem Th2: :: YELLOW17:2

for F, f being Function

for i, xi being set st xi in F . i & f in product F holds

f +* (i,xi) in product F

for i, xi being set st xi in F . i & f in product F holds

f +* (i,xi) in product F

proof end;

theorem Th3: :: YELLOW17:3

for F being Function

for i being set st i in dom F holds

( rng (proj (F,i)) c= F . i & ( product F <> {} implies rng (proj (F,i)) = F . i ) )

for i being set st i in dom F holds

( rng (proj (F,i)) c= F . i & ( product F <> {} implies rng (proj (F,i)) = F . i ) )

proof end;

theorem Th5: :: YELLOW17:5

for F, f being Function

for i, xi being set st xi in F . i & i in dom F & f in product F holds

f +* (i,xi) in (proj (F,i)) " {xi}

for i, xi being set st xi in F . i & i in dom F & f in product F holds

f +* (i,xi) in (proj (F,i)) " {xi}

proof end;

Lm1: for F, g being Function

for i1, i2, xi1 being set

for Ai2 being Subset of (F . i2) st i1 <> i2 & g in product F & g +* (i1,xi1) in (proj (F,i2)) " Ai2 holds

g in (proj (F,i2)) " Ai2

proof end;

theorem Th6: :: YELLOW17:6

for F, f being Function

for i1, i2, xi1 being set

for Ai2 being Subset of (F . i2) st xi1 in F . i1 & f in product F & i1 <> i2 holds

( f in (proj (F,i2)) " Ai2 iff f +* (i1,xi1) in (proj (F,i2)) " Ai2 )

for i1, i2, xi1 being set

for Ai2 being Subset of (F . i2) st xi1 in F . i1 & f in product F & i1 <> i2 holds

( f in (proj (F,i2)) " Ai2 iff f +* (i1,xi1) in (proj (F,i2)) " Ai2 )

proof end;

theorem Th7: :: YELLOW17:7

for F being Function

for i1, i2, xi1 being set

for Ai2 being Subset of (F . i2) st product F <> {} & xi1 in F . i1 & i1 in dom F & i2 in dom F & Ai2 <> F . i2 holds

( (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )

for i1, i2, xi1 being set

for Ai2 being Subset of (F . i2) st product F <> {} & xi1 in F . i1 & i1 in dom F & i2 in dom F & Ai2 <> F . i2 holds

( (proj (F,i1)) " {xi1} c= (proj (F,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )

proof end;

scheme :: YELLOW17:sch 1

ElProductEx{ F_{1}() -> non empty set , F_{2}() -> non-Empty TopStruct-yielding ManySortedSet of F_{1}(), P_{1}[ object , object ] } :

provided

ElProductEx{ F

provided

proof end;

theorem Th8: :: YELLOW17:8

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I

for f being Element of (product J) holds (proj (J,i)) . f = f . i

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I

for f being Element of (product J) holds (proj (J,i)) . f = f . i

proof end;

theorem Th9: :: YELLOW17:9

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I

for xi being Element of (J . i)

for Ai being Subset of (J . i) st (proj (J,i)) " {xi} meets (proj (J,i)) " Ai holds

xi in Ai

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I

for xi being Element of (J . i)

for Ai being Subset of (J . i) st (proj (J,i)) " {xi} meets (proj (J,i)) " Ai holds

xi in Ai

proof end;

theorem Th10: :: YELLOW17:10

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I holds (proj (J,i)) " ([#] (J . i)) = [#] (product J)

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I holds (proj (J,i)) " ([#] (J . i)) = [#] (product J)

proof end;

theorem Th11: :: YELLOW17:11

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I

for xi being Element of (J . i)

for f being Element of (product J) holds f +* (i,xi) in (proj (J,i)) " {xi}

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I

for xi being Element of (J . i)

for f being Element of (product J) holds f +* (i,xi) in (proj (J,i)) " {xi}

proof end;

theorem Th12: :: YELLOW17:12

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i1, i2 being Element of I

for xi1 being Element of (J . i1)

for Ai2 being Subset of (J . i2) st Ai2 <> [#] (J . i2) holds

( (proj (J,i1)) " {xi1} c= (proj (J,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i1, i2 being Element of I

for xi1 being Element of (J . i1)

for Ai2 being Subset of (J . i2) st Ai2 <> [#] (J . i2) holds

( (proj (J,i1)) " {xi1} c= (proj (J,i2)) " Ai2 iff ( i1 = i2 & xi1 in Ai2 ) )

proof end;

theorem Th13: :: YELLOW17:13

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i1, i2 being Element of I

for xi1 being Element of (J . i1)

for Ai2 being Subset of (J . i2)

for f being Element of (product J) st i1 <> i2 holds

( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 )

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i1, i2 being Element of I

for xi1 being Element of (J . i1)

for Ai2 being Subset of (J . i2)

for f being Element of (product J) st i1 <> i2 holds

( f in (proj (J,i2)) " Ai2 iff f +* (i1,xi1) in (proj (J,i2)) " Ai2 )

proof end;

theorem Th14: :: YELLOW17:14

for T being non empty TopStruct holds

( T is compact iff for F being Subset-Family of T st F is open & [#] T c= union F holds

ex G being Subset-Family of T st

( G c= F & [#] T c= union G & G is finite ) )

( T is compact iff for F being Subset-Family of T st F is open & [#] T c= union F holds

ex G being Subset-Family of T st

( G c= F & [#] T c= union G & G is finite ) )

proof end;

theorem Th15: :: YELLOW17:15

for T being non empty TopSpace

for B being prebasis of T holds

( T is compact iff for F being Subset of B st [#] T c= union F holds

ex G being finite Subset of F st [#] T c= union G )

for B being prebasis of T holds

( T is compact iff for F being Subset of B st [#] T c= union F holds

ex G being finite Subset of F st [#] T c= union G )

proof end;

theorem Th16: :: YELLOW17:16

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I

for A being set st A in product_prebasis J holds

ex i being Element of I ex Ai being Subset of (J . i) st

( Ai is open & (proj (J,i)) " Ai = A )

for J being non-Empty TopStruct-yielding ManySortedSet of I

for A being set st A in product_prebasis J holds

ex i being Element of I ex Ai being Subset of (J . i) st

( Ai is open & (proj (J,i)) " Ai = A )

proof end;

theorem Th17: :: YELLOW17:17

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I

for xi being Element of (J . i)

for A being set st A in product_prebasis J & (proj (J,i)) " {xi} c= A & not A = [#] (product J) holds

ex Ai being Subset of (J . i) st

( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj (J,i)) " Ai )

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I

for xi being Element of (J . i)

for A being set st A in product_prebasis J & (proj (J,i)) " {xi} c= A & not A = [#] (product J) holds

ex Ai being Subset of (J . i) st

( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj (J,i)) " Ai )

proof end;

theorem Th18: :: YELLOW17:18

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I

for Fi being non empty Subset-Family of (J . i) st [#] (J . i) c= union Fi holds

[#] (product J) c= union { ((proj (J,i)) " Ai) where Ai is Element of Fi : verum }

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I

for Fi being non empty Subset-Family of (J . i) st [#] (J . i) c= union Fi holds

[#] (product J) c= union { ((proj (J,i)) " Ai) where Ai is Element of Fi : verum }

proof end;

theorem Th19: :: YELLOW17:19

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I

for xi being Element of (J . i)

for G being Subset of (product_prebasis J) st (proj (J,i)) " {xi} c= union G & ( for A being set st A in product_prebasis J & A in G holds

not (proj (J,i)) " {xi} c= A ) holds

[#] (product J) c= union G

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I

for xi being Element of (J . i)

for G being Subset of (product_prebasis J) st (proj (J,i)) " {xi} c= union G & ( for A being set st A in product_prebasis J & A in G holds

not (proj (J,i)) " {xi} c= A ) holds

[#] (product J) c= union G

proof end;

theorem Th20: :: YELLOW17:20

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I

for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds

for xi being Element of (J . i)

for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds

ex A being set st

( A in product_prebasis J & A in G & (proj (J,i)) " {xi} c= A )

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I

for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds

for xi being Element of (J . i)

for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds

ex A being set st

( A in product_prebasis J & A in G & (proj (J,i)) " {xi} c= A )

proof end;

theorem Th21: :: YELLOW17:21

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I

for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds

for xi being Element of (J . i)

for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds

ex Ai being Subset of (J . i) st

( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I

for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds

for xi being Element of (J . i)

for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds

ex Ai being Subset of (J . i) st

( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )

proof end;

theorem Th22: :: YELLOW17:22

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I

for F being Subset of (product_prebasis J) st ( for i being Element of I holds J . i is compact ) & ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds

ex xi being Element of (J . i) st

for G being finite Subset of F holds not (proj (J,i)) " {xi} c= union G

for J being non-Empty TopStruct-yielding ManySortedSet of I

for i being Element of I

for F being Subset of (product_prebasis J) st ( for i being Element of I holds J . i is compact ) & ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds

ex xi being Element of (J . i) st

for G being finite Subset of F holds not (proj (J,i)) " {xi} c= union G

proof end;

:: Tychonoff's theorem

theorem :: YELLOW17:23

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds J . i is compact ) holds

product J is compact

for J being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds J . i is compact ) holds

product J is compact

proof end;