:: REALSET1 semantic presentation begin theorem Th1: :: REALSET1:1 for X, x being set for F being Function of [:X,X:],X st x in [:X,X:] holds F . x in X proof let X, x be set ; ::_thesis: for F being Function of [:X,X:],X st x in [:X,X:] holds F . x in X let F be Function of [:X,X:],X; ::_thesis: ( x in [:X,X:] implies F . x in X ) ( X = {} implies [:X,X:] = {} ) ; then A1: dom F = [:X,X:] by FUNCT_2:def_1; assume x in [:X,X:] ; ::_thesis: F . x in X then ( rng F c= X & F . x in rng F ) by A1, FUNCT_1:def_3, RELAT_1:def_19; hence F . x in X ; ::_thesis: verum end; definition let X be set ; let F be BinOp of X; mode Preserv of F -> Subset of X means :Def1: :: REALSET1:def 1 for x being set st x in [:it,it:] holds F . x in it; existence ex b1 being Subset of X st for x being set st x in [:b1,b1:] holds F . x in b1 proof X c= X ; then reconsider Z = X as Subset of X ; take Z ; ::_thesis: for x being set st x in [:Z,Z:] holds F . x in Z thus for x being set st x in [:Z,Z:] holds F . x in Z by Th1; ::_thesis: verum end; end; :: deftheorem Def1 defines Preserv REALSET1:def_1_:_ for X being set for F being BinOp of X for b3 being Subset of X holds ( b3 is Preserv of F iff for x being set st x in [:b3,b3:] holds F . x in b3 ); definition let R be Relation; let A be set ; funcR || A -> set equals :: REALSET1:def 2 R | [:A,A:]; coherence R | [:A,A:] is set ; end; :: deftheorem defines || REALSET1:def_2_:_ for R being Relation for A being set holds R || A = R | [:A,A:]; registration let R be Relation; let A be set ; clusterR || A -> Relation-like ; coherence R || A is Relation-like ; end; registration let R be Function; let A be set ; clusterR || A -> Function-like ; coherence R || A is Function-like ; end; theorem Th2: :: REALSET1:2 for X being set for F being BinOp of X for A being Preserv of F holds F || A is BinOp of A proof let X be set ; ::_thesis: for F being BinOp of X for A being Preserv of F holds F || A is BinOp of A let F be BinOp of X; ::_thesis: for A being Preserv of F holds F || A is BinOp of A let A be Preserv of F; ::_thesis: F || A is BinOp of A ( X = {} implies [:X,X:] = {} ) ; then dom F = [:X,X:] by FUNCT_2:def_1; then A1: dom (F || A) = [:A,A:] by RELAT_1:62, ZFMISC_1:96; for x being set st x in [:A,A:] holds (F || A) . x in A proof let x be set ; ::_thesis: ( x in [:A,A:] implies (F || A) . x in A ) assume A2: x in [:A,A:] ; ::_thesis: (F || A) . x in A then (F || A) . x = F . x by A1, FUNCT_1:47; hence (F || A) . x in A by A2, Def1; ::_thesis: verum end; hence F || A is BinOp of A by A1, FUNCT_2:3; ::_thesis: verum end; definition let X be set ; let F be BinOp of X; let A be Preserv of F; :: original: || redefine funcF || A -> BinOp of A; coherence F || A is BinOp of A by Th2; end; theorem Th3: :: REALSET1:3 for X being set holds ( not X is trivial iff for x being set holds X \ {x} is non empty set ) proof let X be set ; ::_thesis: ( not X is trivial iff for x being set holds X \ {x} is non empty set ) hereby ::_thesis: ( ( for x being set holds X \ {x} is non empty set ) implies not X is trivial ) assume A1: not X is trivial ; ::_thesis: for x being set holds X \ {x} is non empty set let x be set ; ::_thesis: X \ {x} is non empty set X <> {x} by A1; then consider y being set such that A2: y in X and A3: x <> y by A1, ZFMISC_1:35; not y in {x} by A3, TARSKI:def_1; hence X \ {x} is non empty set by A2, XBOOLE_0:def_5; ::_thesis: verum end; assume A4: for x being set holds X \ {x} is non empty set ; ::_thesis: not X is trivial X \ {{}} c= X ; then not X is empty by A4; then consider x being set such that A5: x in X by XBOOLE_0:def_1; not X \ {x} is empty by A4; then consider y being set such that A6: y in X \ {x} by XBOOLE_0:def_1; take x ; :: according to ZFMISC_1:def_10 ::_thesis: ex b1 being set st ( x in X & b1 in X & not x = b1 ) take y ; ::_thesis: ( x in X & y in X & not x = y ) thus x in X by A5; ::_thesis: ( y in X & not x = y ) thus y in X by A6; ::_thesis: not x = y x in {x} by TARSKI:def_1; then not x in X \ {x} by XBOOLE_0:def_5; hence x <> y by A6; ::_thesis: verum end; theorem :: REALSET1:4 ex A being non empty set st for z being Element of A holds A \ {z} is non empty set proof set B = {0,1}; take {0,1} ; ::_thesis: for z being Element of {0,1} holds {0,1} \ {z} is non empty set for z being Element of {0,1} holds {0,1} \ {z} is non empty set proof let z be Element of {0,1}; ::_thesis: {0,1} \ {z} is non empty set ( 0 in {0,1} & not 0 in {1} ) by TARSKI:def_1, TARSKI:def_2; then A1: {0,1} \ {1} is non empty set by XBOOLE_0:def_5; ( 1 in {0,1} & not 1 in {0} ) by TARSKI:def_1, TARSKI:def_2; then {0,1} \ {0} is non empty set by XBOOLE_0:def_5; hence {0,1} \ {z} is non empty set by A1, TARSKI:def_2; ::_thesis: verum end; hence for z being Element of {0,1} holds {0,1} \ {z} is non empty set ; ::_thesis: verum end; definition let X be non trivial set ; let F be BinOp of X; let x be Element of X; predF is_Bin_Op_Preserv x means :: REALSET1:def 3 ( X \ {x} is Preserv of F & (F || X) \ {x} is BinOp of (X \ {x}) ); correctness ; end; :: deftheorem defines is_Bin_Op_Preserv REALSET1:def_3_:_ for X being non trivial set for F being BinOp of X for x being Element of X holds ( F is_Bin_Op_Preserv x iff ( X \ {x} is Preserv of F & (F || X) \ {x} is BinOp of (X \ {x}) ) ); theorem Th5: :: REALSET1:5 for X being set for A being Subset of X ex F being BinOp of X st for x being set st x in [:A,A:] holds F . x in A proof let X be set ; ::_thesis: for A being Subset of X ex F being BinOp of X st for x being set st x in [:A,A:] holds F . x in A let A be Subset of X; ::_thesis: ex F being BinOp of X st for x being set st x in [:A,A:] holds F . x in A set S = pr1 (X,X); take pr1 (X,X) ; ::_thesis: for x being set st x in [:A,A:] holds (pr1 (X,X)) . x in A for x being set st x in [:A,A:] holds (pr1 (X,X)) . x in A proof let x be set ; ::_thesis: ( x in [:A,A:] implies (pr1 (X,X)) . x in A ) assume x in [:A,A:] ; ::_thesis: (pr1 (X,X)) . x in A then consider p, q being set such that A1: ( p in A & q in A ) and A2: x = [p,q] by ZFMISC_1:def_2; (pr1 (X,X)) . x = (pr1 (X,X)) . (p,q) by A2; hence (pr1 (X,X)) . x in A by A1, FUNCT_3:def_4; ::_thesis: verum end; hence for x being set st x in [:A,A:] holds (pr1 (X,X)) . x in A ; ::_thesis: verum end; definition let X be set ; let A be Subset of X; mode Presv of X,A -> BinOp of X means :Def4: :: REALSET1:def 4 for x being set st x in [:A,A:] holds it . x in A; existence ex b1 being BinOp of X st for x being set st x in [:A,A:] holds b1 . x in A by Th5; end; :: deftheorem Def4 defines Presv REALSET1:def_4_:_ for X being set for A being Subset of X for b3 being BinOp of X holds ( b3 is Presv of X,A iff for x being set st x in [:A,A:] holds b3 . x in A ); theorem Th6: :: REALSET1:6 for X being set for A being Subset of X for F being Presv of X,A holds F || A is BinOp of A proof let X be set ; ::_thesis: for A being Subset of X for F being Presv of X,A holds F || A is BinOp of A let A be Subset of X; ::_thesis: for F being Presv of X,A holds F || A is BinOp of A let F be Presv of X,A; ::_thesis: F || A is BinOp of A ( X = {} implies [:X,X:] = {} ) ; then dom F = [:X,X:] by FUNCT_2:def_1; then A1: dom (F || A) = [:A,A:] by RELAT_1:62, ZFMISC_1:96; for x being set st x in [:A,A:] holds (F || A) . x in A proof let x be set ; ::_thesis: ( x in [:A,A:] implies (F || A) . x in A ) assume A2: x in [:A,A:] ; ::_thesis: (F || A) . x in A then (F || A) . x = F . x by A1, FUNCT_1:47; hence (F || A) . x in A by A2, Def4; ::_thesis: verum end; hence F || A is BinOp of A by A1, FUNCT_2:3; ::_thesis: verum end; definition let X be set ; let A be Subset of X; let F be Presv of X,A; funcF ||| A -> BinOp of A equals :: REALSET1:def 5 F || A; coherence F || A is BinOp of A by Th6; end; :: deftheorem defines ||| REALSET1:def_5_:_ for X being set for A being Subset of X for F being Presv of X,A holds F ||| A = F || A; definition let A be set ; let x be Element of A; mode DnT of x,A -> BinOp of A means :Def6: :: REALSET1:def 6 for y being set st y in [:(A \ {x}),(A \ {x}):] holds it . y in A \ {x}; existence ex b1 being BinOp of A st for y being set st y in [:(A \ {x}),(A \ {x}):] holds b1 . y in A \ {x} by Th5; end; :: deftheorem Def6 defines DnT REALSET1:def_6_:_ for A being set for x being Element of A for b3 being BinOp of A holds ( b3 is DnT of x,A iff for y being set st y in [:(A \ {x}),(A \ {x}):] holds b3 . y in A \ {x} ); theorem Th7: :: REALSET1:7 for A being non trivial set for x being Element of A for F being DnT of x,A holds F || (A \ {x}) is BinOp of (A \ {x}) proof let A be non trivial set ; ::_thesis: for x being Element of A for F being DnT of x,A holds F || (A \ {x}) is BinOp of (A \ {x}) let x be Element of A; ::_thesis: for F being DnT of x,A holds F || (A \ {x}) is BinOp of (A \ {x}) let F be DnT of x,A; ::_thesis: F || (A \ {x}) is BinOp of (A \ {x}) dom F = [:A,A:] by FUNCT_2:def_1; then A1: dom (F || (A \ {x})) = [:(A \ {x}),(A \ {x}):] by RELAT_1:62, ZFMISC_1:96; for y being set st y in [:(A \ {x}),(A \ {x}):] holds (F || (A \ {x})) . y in A \ {x} proof let y be set ; ::_thesis: ( y in [:(A \ {x}),(A \ {x}):] implies (F || (A \ {x})) . y in A \ {x} ) assume A2: y in [:(A \ {x}),(A \ {x}):] ; ::_thesis: (F || (A \ {x})) . y in A \ {x} then (F || (A \ {x})) . y = F . y by A1, FUNCT_1:47; hence (F || (A \ {x})) . y in A \ {x} by A2, Def6; ::_thesis: verum end; hence F || (A \ {x}) is BinOp of (A \ {x}) by A1, FUNCT_2:3; ::_thesis: verum end; definition let A be non trivial set ; let x be Element of A; let F be DnT of x,A; funcF ! (A,x) -> BinOp of (A \ {x}) equals :: REALSET1:def 7 F || (A \ {x}); coherence F || (A \ {x}) is BinOp of (A \ {x}) by Th7; end; :: deftheorem defines ! REALSET1:def_7_:_ for A being non trivial set for x being Element of A for F being DnT of x,A holds F ! (A,x) = F || (A \ {x}); theorem Th8: :: REALSET1:8 for F being non trivial set for A being Singleton of F holds F \ A is non empty set proof let F be non trivial set ; ::_thesis: for A being Singleton of F holds F \ A is non empty set let A be Singleton of F; ::_thesis: F \ A is non empty set ex x being Element of F st A = {x} by CARD_1:65; hence F \ A is non empty set by Th3; ::_thesis: verum end; registration let F be non trivial set ; let A be Singleton of F; clusterF \ A -> non empty ; coherence not F \ A is empty by Th8; end;