:: by Adam Grabowski and Robert Milewski

::

:: Received September 20, 1996

:: Copyright (c) 1996-2012 Association of Mizar Users

begin

registration

let L be Lattice;

coherence

( LattPOSet L is with_suprema & LattPOSet L is with_infima ) by LATTICE3:11;

end;
coherence

( LattPOSet L is with_suprema & LattPOSet L is with_infima ) by LATTICE3:11;

definition

let X be set ;

:: original: RelIncl

redefine func RelIncl X -> Order of X;

coherence

RelIncl X is Order of X

end;
:: original: RelIncl

redefine func RelIncl X -> Order of X;

coherence

RelIncl X is Order of X

proof end;

:: deftheorem defines InclPoset YELLOW_1:def 1 :

for X being set holds InclPoset X = RelStr(# X,(RelIncl X) #);

for X being set holds InclPoset X = RelStr(# X,(RelIncl X) #);

registration

let X be set ;

coherence

( InclPoset X is reflexive & InclPoset X is antisymmetric & InclPoset X is transitive ) ;

end;
coherence

( InclPoset X is reflexive & InclPoset X is antisymmetric & InclPoset X is transitive ) ;

theorem :: YELLOW_1:1

:: deftheorem defines BoolePoset YELLOW_1:def 2 :

for X being set holds BoolePoset X = LattPOSet (BooleLatt X);

for X being set holds BoolePoset X = LattPOSet (BooleLatt X);

registration

let X be set ;

coherence

( not BoolePoset X is empty & BoolePoset X is reflexive & BoolePoset X is antisymmetric & BoolePoset X is transitive ) ;

end;
coherence

( not BoolePoset X is empty & BoolePoset X is reflexive & BoolePoset X is antisymmetric & BoolePoset X is transitive ) ;

registration
end;

theorem :: YELLOW_1:6

for X being non empty set st InclPoset X is with_suprema holds

for x, y being Element of (InclPoset X) holds x \/ y c= x "\/" y

for x, y being Element of (InclPoset X) holds x \/ y c= x "\/" y

proof end;

theorem :: YELLOW_1:7

for X being non empty set st InclPoset X is with_infima holds

for x, y being Element of (InclPoset X) holds x "/\" y c= x /\ y

for x, y being Element of (InclPoset X) holds x "/\" y c= x /\ y

proof end;

theorem Th8: :: YELLOW_1:8

for X being non empty set

for x, y being Element of (InclPoset X) st x \/ y in X holds

x "\/" y = x \/ y

for x, y being Element of (InclPoset X) st x \/ y in X holds

x "\/" y = x \/ y

proof end;

theorem Th9: :: YELLOW_1:9

for X being non empty set

for x, y being Element of (InclPoset X) st x /\ y in X holds

x "/\" y = x /\ y

for x, y being Element of (InclPoset X) st x /\ y in X holds

x "/\" y = x /\ y

proof end;

theorem :: YELLOW_1:10

for L being RelStr st ( for x, y being Element of L holds

( x <= y iff x c= y ) ) holds

the InternalRel of L = RelIncl the carrier of L

( x <= y iff x c= y ) ) holds

the InternalRel of L = RelIncl the carrier of L

proof end;

theorem :: YELLOW_1:11

for X being non empty set st ( for x, y being set st x in X & y in X holds

x \/ y in X ) holds

InclPoset X is with_suprema

x \/ y in X ) holds

InclPoset X is with_suprema

proof end;

theorem :: YELLOW_1:12

for X being non empty set st ( for x, y being set st x in X & y in X holds

x /\ y in X ) holds

InclPoset X is with_infima

x /\ y in X ) holds

InclPoset X is with_infima

proof end;

Lm1: for X being set

for x, y being Element of (BoolePoset X) holds

( x /\ y in bool X & x \/ y in bool X )

proof end;

theorem :: YELLOW_1:17

for X being set

for x, y being Element of (BoolePoset X) holds

( x "\/" y = x \/ y & x "/\" y = x /\ y )

for x, y being Element of (BoolePoset X) holds

( x "\/" y = x \/ y & x "/\" y = x /\ y )

proof end;

theorem :: YELLOW_1:22

for T being non empty TopSpace

for X being Subset of (InclPoset the topology of T) holds sup X = union X

for X being Subset of (InclPoset the topology of T) holds sup X = union X

proof end;

theorem :: YELLOW_1:23

Lm2: for T being non empty TopSpace holds InclPoset the topology of T is lower-bounded

proof end;

Lm3: for T being non empty TopSpace holds InclPoset the topology of T is complete

proof end;

Lm4: for T being non empty TopSpace holds not InclPoset the topology of T is trivial

proof end;

registration

let T be non empty TopSpace;

coherence

( InclPoset the topology of T is complete & not InclPoset the topology of T is trivial ) by Lm3, Lm4;

end;
coherence

( InclPoset the topology of T is complete & not InclPoset the topology of T is trivial ) by Lm3, Lm4;

theorem :: YELLOW_1:25

for T being TopSpace

for F being Subset-Family of T holds

( F is open iff F is Subset of (InclPoset the topology of T) )

for F being Subset-Family of T holds

( F is open iff F is Subset of (InclPoset the topology of T) )

proof end;

begin

definition

let R be Relation;

end;
attr R is RelStr-yielding means :Def3: :: YELLOW_1:def 3

for v being set st v in rng R holds

v is RelStr ;

for v being set st v in rng R holds

v is RelStr ;

:: deftheorem Def3 defines RelStr-yielding YELLOW_1:def 3 :

for R being Relation holds

( R is RelStr-yielding iff for v being set st v in rng R holds

v is RelStr );

for R being Relation holds

( R is RelStr-yielding iff for v being set st v in rng R holds

v is RelStr );

registration

coherence

for b_{1} being Function st b_{1} is RelStr-yielding holds

b_{1} is 1-sorted-yielding

end;
for b

b

proof end;

registration
end;

definition

let J be non empty set ;

let A be RelStr-yielding ManySortedSet of J;

let j be Element of J;

:: original: .

redefine func A . j -> RelStr ;

coherence

A . j is RelStr

end;
let A be RelStr-yielding ManySortedSet of J;

let j be Element of J;

:: original: .

redefine func A . j -> RelStr ;

coherence

A . j is RelStr

proof end;

definition

let I be set ;

let J be RelStr-yielding ManySortedSet of I;

ex b_{1} being strict RelStr st

( the carrier of b_{1} = product (Carrier J) & ( for x, y being Element of b_{1} st x in product (Carrier J) holds

( x <= y iff ex f, g being Function st

( f = x & g = y & ( for i being set st i in I holds

ex R being RelStr ex xi, yi being Element of R st

( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) )

for b_{1}, b_{2} being strict RelStr st the carrier of b_{1} = product (Carrier J) & ( for x, y being Element of b_{1} st x in product (Carrier J) holds

( x <= y iff ex f, g being Function st

( f = x & g = y & ( for i being set st i in I holds

ex R being RelStr ex xi, yi being Element of R st

( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) & the carrier of b_{2} = product (Carrier J) & ( for x, y being Element of b_{2} st x in product (Carrier J) holds

( x <= y iff ex f, g being Function st

( f = x & g = y & ( for i being set st i in I holds

ex R being RelStr ex xi, yi being Element of R st

( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) holds

b_{1} = b_{2}

end;
let J be RelStr-yielding ManySortedSet of I;

func product J -> strict RelStr means :Def4: :: YELLOW_1:def 4

( the carrier of it = product (Carrier J) & ( for x, y being Element of it st x in product (Carrier J) holds

( x <= y iff ex f, g being Function st

( f = x & g = y & ( for i being set st i in I holds

ex R being RelStr ex xi, yi being Element of R st

( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) );

existence ( the carrier of it = product (Carrier J) & ( for x, y being Element of it st x in product (Carrier J) holds

( x <= y iff ex f, g being Function st

( f = x & g = y & ( for i being set st i in I holds

ex R being RelStr ex xi, yi being Element of R st

( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) );

ex b

( the carrier of b

( x <= y iff ex f, g being Function st

( f = x & g = y & ( for i being set st i in I holds

ex R being RelStr ex xi, yi being Element of R st

( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) )

proof end;

uniqueness for b

( x <= y iff ex f, g being Function st

( f = x & g = y & ( for i being set st i in I holds

ex R being RelStr ex xi, yi being Element of R st

( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) & the carrier of b

( x <= y iff ex f, g being Function st

( f = x & g = y & ( for i being set st i in I holds

ex R being RelStr ex xi, yi being Element of R st

( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) holds

b

proof end;

:: deftheorem Def4 defines product YELLOW_1:def 4 :

for I being set

for J being RelStr-yielding ManySortedSet of I

for b_{3} being strict RelStr holds

( b_{3} = product J iff ( the carrier of b_{3} = product (Carrier J) & ( for x, y being Element of b_{3} st x in product (Carrier J) holds

( x <= y iff ex f, g being Function st

( f = x & g = y & ( for i being set st i in I holds

ex R being RelStr ex xi, yi being Element of R st

( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) ) );

for I being set

for J being RelStr-yielding ManySortedSet of I

for b

( b

( x <= y iff ex f, g being Function st

( f = x & g = y & ( for i being set st i in I holds

ex R being RelStr ex xi, yi being Element of R st

( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) ) );

definition
end;

:: deftheorem defines |^ YELLOW_1:def 5 :

for I being set

for T being RelStr holds T |^ I = product (I --> T);

for I being set

for T being RelStr holds T |^ I = product (I --> T);

registration
end;

Lm5: for X being set

for Y being non empty RelStr

for x being Element of (Y |^ X) holds

( x in the carrier of (product (X --> Y)) & x is Function of X, the carrier of Y )

proof end;

registration
end;

registration

let Y be non empty reflexive RelStr ;

coherence

( Y |^ {} is with_infima & Y |^ {} is with_suprema & Y |^ {} is antisymmetric ) ;

end;
coherence

( Y |^ {} is with_infima & Y |^ {} is with_suprema & Y |^ {} is antisymmetric ) ;

registration
end;

registration

let X be set ;

let Y be non empty antisymmetric RelStr ;

coherence

Y |^ X is antisymmetric

end;
let Y be non empty antisymmetric RelStr ;

coherence

Y |^ X is antisymmetric

proof end;

registration

let X be non empty set ;

let Y be non empty antisymmetric with_infima RelStr ;

coherence

Y |^ X is with_infima

end;
let Y be non empty antisymmetric with_infima RelStr ;

coherence

Y |^ X is with_infima

proof end;

registration

let X be non empty set ;

let Y be non empty antisymmetric with_suprema RelStr ;

coherence

Y |^ X is with_suprema

end;
let Y be non empty antisymmetric with_suprema RelStr ;

coherence

Y |^ X is with_suprema

proof end;

definition

let S, T be RelStr ;

ex b_{1} being strict full SubRelStr of T |^ the carrier of S st

for f being Function of S,T holds

( f in the carrier of b_{1} iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) )

for b_{1}, b_{2} being strict full SubRelStr of T |^ the carrier of S st ( for f being Function of S,T holds

( f in the carrier of b_{1} iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ) ) & ( for f being Function of S,T holds

( f in the carrier of b_{2} iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ) ) holds

b_{1} = b_{2}

end;
func MonMaps (S,T) -> strict full SubRelStr of T |^ the carrier of S means :: YELLOW_1:def 6

for f being Function of S,T holds

( f in the carrier of it iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) );

existence for f being Function of S,T holds

( f in the carrier of it iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) );

ex b

for f being Function of S,T holds

( f in the carrier of b

proof end;

uniqueness for b

( f in the carrier of b

( f in the carrier of b

b

proof end;

:: deftheorem defines MonMaps YELLOW_1:def 6 :

for S, T being RelStr

for b_{3} being strict full SubRelStr of T |^ the carrier of S holds

( b_{3} = MonMaps (S,T) iff for f being Function of S,T holds

( f in the carrier of b_{3} iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ) );

for S, T being RelStr

for b

( b

( f in the carrier of b