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 ) )
assume A1: B = union A ; :: thesis: ( A is closed iff B is closed )
reconsider C = A as Subset of S by BORSUK_1:def 10;
A2: ([#] T) \ (union A) = (union S) \ (union C) by EQREL_1:def 6
.= union (S \ A) by EQREL_1:52
.= union (([#] (space S)) \ A) by BORSUK_1:def 10 ;
thus ( A is closed implies B is closed ) :: thesis: ( B is closed implies A is closed )

proof

assume A is closed ; :: thesis: B is closed
then A3: ([#] (space S)) \ A is open by PRE_TOPC:def 6;
reconsider om = ([#] (space S)) \ A as Subset of S by BORSUK_1:def 10;
om in the topology of (space S) by A3, PRE_TOPC:def 5;
then ([#] T) \ B in the topology of T by A1, A2, BORSUK_1:69;
then ([#] T) \ B is open by PRE_TOPC:def 5;
hence B is closed by PRE_TOPC:def 6; :: thesis: verum

end;

thus ( B is closed implies A is closed ) :: thesis: verum

proof

assume B is closed ; :: thesis: A is closed
then ([#] T) \ B is open by PRE_TOPC:def 6;
then A4: ([#] T) \ (union A) in the topology of T by A1, PRE_TOPC:def 5;
reconsider om = ([#] (space S)) \ A as Subset of S by BORSUK_1:def 10;
om in the topology of (space S) by A2, A4, BORSUK_1:69;
then ([#] (space S)) \ A is open by PRE_TOPC:def 5;
hence A is closed by PRE_TOPC:def 6; :: thesis: verum

end;