let T be non empty TopSpace; :: thesis: for S being non empty a_partition of the carrier of T
for A being Subset of (space S)
for B being Subset of T st B = union A holds
( A is closed iff B is closed )
let S be non empty a_partition of the carrier of T; :: thesis: for A being Subset of (space S)
for B being Subset of T st B = union A holds
( A is closed iff B is closed )
let A be Subset of (space S); :: thesis: for B being Subset of T st B = union A holds
( A is closed iff B is closed )
let B be Subset of T; :: thesis: ( B = union A implies ( A is closed iff B is closed ) )
reconsider C = A as Subset of S by BORSUK_1:def 7;
A1: ([#] T) \ (union A) = (union S) \ (union C) by EQREL_1:def 4
.= union (S \ A) by EQREL_1:43
.= union (([#] (space S)) \ A) by BORSUK_1:def 7 ;
assume A2: B = union A ; :: thesis: ( A is closed iff B is closed )
thus ( A is closed implies B is closed ) :: thesis: ( B is closed implies A is closed )
proof
reconsider om = ([#] (space S)) \ A as Subset of S by BORSUK_1:def 7;
assume A is closed ; :: thesis: B is closed
then ([#] (space S)) \ A is open ;
then om in the topology of (space S) ;
then ([#] T) \ B in the topology of T by A2, A1, BORSUK_1:27;
then ([#] T) \ B is open ;
hence B is closed ; :: thesis: verum
end;
thus ( B is closed implies A is closed ) :: thesis: verum
proof
reconsider om = ([#] (space S)) \ A as Subset of S by BORSUK_1:def 7;
assume B is closed ; :: thesis: A is closed
then ([#] T) \ B is open ;
then ([#] T) \ (union A) in the topology of T by A2;
then om in the topology of (space S) by A1, BORSUK_1:27;
then ([#] (space S)) \ A is open ;
hence A is closed ; :: thesis: verum
end;