set f = AffineMap (1,0,(1 / 2),(- (1 / 2)));
set A = 1;
set B = 0 ;
set C = 1 / 2;
set D = - (1 / 2);
let S, T be Subset of (TOP-REAL 2); ( S = { p where p is Point of (TOP-REAL 2) : p `2 >= 1 - (2 * (p `1)) } & T = { p where p is Point of (TOP-REAL 2) : p `2 >= - (p `1) } implies (AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: S = T )
assume that
A1:
S = { p where p is Point of (TOP-REAL 2) : p `2 >= 1 - (2 * (p `1)) }
and
A2:
T = { p where p is Point of (TOP-REAL 2) : p `2 >= - (p `1) }
; (AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: S = T
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: S = T
proof
thus
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: S c= T
XBOOLE_0:def 10 T c= (AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: Sproof
let x be
object ;
TARSKI:def 3 ( not x in (AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: S or x in T )
assume
x in (AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: S
;
x in T
then consider y being
object such that
y in dom (AffineMap (1,0,(1 / 2),(- (1 / 2))))
and A3:
y in S
and A4:
x = (AffineMap (1,0,(1 / 2),(- (1 / 2)))) . y
by FUNCT_1:def 6;
consider p being
Point of
(TOP-REAL 2) such that A5:
y = p
and A6:
p `2 >= 1
- (2 * (p `1))
by A1, A3;
set b =
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) . p;
(1 / 2) * (p `2) >= (1 / 2) * (1 - (2 * (p `1)))
by A6, XREAL_1:64;
then A7:
((1 / 2) * (p `2)) + (- (1 / 2)) >= ((1 / 2) - (p `1)) + (- (1 / 2))
by XREAL_1:6;
A8:
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) . p = |[((1 * (p `1)) + 0),(((1 / 2) * (p `2)) + (- (1 / 2)))]|
by JGRAPH_2:def 2;
then
((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . p) `1 = (1 * (p `1)) + 0
by EUCLID:52;
then
((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . p) `2 >= - (((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . p) `1)
by A8, A7, EUCLID:52;
hence
x in T
by A2, A4, A5;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in T or x in (AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: S )
assume A9:
x in T
;
x in (AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: S
then A10:
ex
p being
Point of
(TOP-REAL 2) st
(
x = p &
p `2 >= - (p `1) )
by A2;
AffineMap (1,
0,
(1 / 2),
(- (1 / 2))) is
onto
by JORDAN1K:36;
then
rng (AffineMap (1,0,(1 / 2),(- (1 / 2)))) = the
carrier of
(TOP-REAL 2)
by FUNCT_2:def 3;
then consider y being
object such that A11:
y in dom (AffineMap (1,0,(1 / 2),(- (1 / 2))))
and A12:
x = (AffineMap (1,0,(1 / 2),(- (1 / 2)))) . y
by A9, FUNCT_1:def 3;
reconsider y =
y as
Point of
(TOP-REAL 2) by A11;
set b =
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) . y;
A13:
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) . y = |[((1 * (y `1)) + 0),(((1 / 2) * (y `2)) + (- (1 / 2)))]|
by JGRAPH_2:def 2;
then
((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . y) `1 = y `1
by EUCLID:52;
then
2
* (((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . y) `2) >= 2
* (- (y `1))
by A10, A12, XREAL_1:64;
then A14:
(2 * (((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . y) `2)) + 1
>= (2 * (- (y `1))) + 1
by XREAL_1:6;
((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . y) `2 = ((1 / 2) * (y `2)) + (- (1 / 2))
by A13, EUCLID:52;
then
y `2 >= 1
- (2 * (y `1))
by A14;
then
y in S
by A1;
hence
x in (AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: S
by A11, A12, FUNCT_1:def 6;
verum
end;
hence
(AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: S = T
; verum