environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, PRE_TOPC, EUCLID, ARYTM_1, ARYTM_3, SUPINF_2, XBOOLE_0, JORDAN2C, RELAT_1, CARD_1, VALUED_0, FINSEQ_1, COMPLEX1, SQUARE_1, CARD_3, RVSUM_1, XXREAL_0, METRIC_1, NAT_1, TARSKI, STRUCT_0, REAL_1, RCOMP_1, XXREAL_2, CONVEX1, RLTOPSP1, FUNCT_1, UNIALG_1, MSSUBFAM, FUNCOP_1, ORDINAL2, JGRAPH_2, MCART_1, PROB_1, FINSEQ_2, FUNCT_3, POLYEQ_1, JGRAPH_6, XCMPLX_0, RLVECT_1, INCSP_1, PENCIL_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, FINSEQ_1, FINSEQ_2, RVSUM_1, VALUED_0, SQUARE_1, QUIN_1, POLYEQ_1, STRUCT_0, PRE_TOPC, METRIC_1, TBSP_1, RLVECT_1, RLTOPSP1, EUCLID, JGRAPH_2, JGRAPH_6, VECTSP_1;
definitions TARSKI, XBOOLE_0, RLTOPSP1, JORDAN1, VECTSP_1;
theorems JGRAPH_6, TOPRNS_1, TARSKI, SUBSET_1, FUNCT_2, EUCLID, JGRAPH_2, XBOOLE_1, XBOOLE_0, FUNCOP_1, JORDAN2C, JORDAN1, SQUARE_1, XCMPLX_1, ABSVALUE, JGRAPH_1, QUIN_1, POLYEQ_1, TOPREAL3, METRIC_1, TOPREAL6, RVSUM_1, EUCLID_2, GOBOARD6, REVROT_1, ENUMSET1, COMPLEX1, XREAL_1, XXREAL_0, RLTOPSP1, RLVECT_1, VECTSP_1, RLVECT_4;
schemes ;
registrations XBOOLE_0, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, STRUCT_0, MONOID_0, EUCLID, TOPALG_2, VALUED_0, FINSEQ_1, FUNCT_1, RELAT_1, PRE_TOPC, TBSP_1, JORDAN2C, QUIN_1, ORDINAL1, RLTOPSP1, CARD_1;
constructors HIDDEN, REAL_1, SQUARE_1, BINOP_2, COMPLEX1, QUIN_1, FINSEQOP, POLYEQ_1, BORSUK_1, TBSP_1, MONOID_0, JGRAPH_2, JGRAPH_6, CONVEX1, GRCAT_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities RLTOPSP1, SQUARE_1, EUCLID, XCMPLX_0, ALGSTR_0, STRUCT_0;
expansions TARSKI, XBOOLE_0, RLTOPSP1;
theorem Th2:
for
r being
Real for
V being
RealLinearSpace for
y,
z being
Point of
V for
x being
object st
x = ((1 - r) * y) + (r * z) holds
( ( not
x = y or
r = 0 or
y = z ) & ( (
r = 0 or
y = z ) implies
x = y ) & ( not
x = z or
r = 1 or
y = z ) & ( (
r = 1 or
y = z ) implies
x = z ) )
Lm1:
for n being Nat
for a being Real
for P being Subset of (TOP-REAL n)
for Q being Point of (TOP-REAL n) st P = { q where q is Point of (TOP-REAL n) : |.(q - Q).| <= a } holds
P is convex
Lm2:
for n being Nat
for a being Real
for P being Subset of (TOP-REAL n)
for Q being Point of (TOP-REAL n) st P = { q where q is Point of (TOP-REAL n) : |.(q - Q).| < a } holds
P is convex
theorem Th35:
for
n being
Nat for
a,
r being
Real for
y,
z,
x being
Point of
(TOP-REAL n) for
S,
T,
X being
Element of
REAL n st
S = y &
T = z &
X = x &
y <> z &
y in Ball (
x,
r) &
a = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) holds
ex
e being
Point of
(TOP-REAL n) st
(
{e} = (halfline (y,z)) /\ (Sphere (x,r)) &
e = ((1 - a) * y) + (a * z) )
theorem Th36:
for
n being
Nat for
a,
r being
Real for
y,
z,
x being
Point of
(TOP-REAL n) for
S,
T,
Y being
Element of
REAL n st
S = ((1 / 2) * y) + ((1 / 2) * z) &
T = z &
Y = x &
y <> z &
y in Sphere (
x,
r) &
z in cl_Ball (
x,
r) holds
ex
e being
Point of
(TOP-REAL n) st
(
e <> y &
{y,e} = (halfline (y,z)) /\ (Sphere (x,r)) & (
z in Sphere (
x,
r) implies
e = z ) & ( not
z in Sphere (
x,
r) &
a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies
e = ((1 - a) * (((1 / 2) * y) + ((1 / 2) * z))) + (a * z) ) )
theorem
for
a,
b,
r,
w being
Real for
s,
t being
Point of
(TOP-REAL 2) for
S,
T,
X being
Element of
REAL 2 st
S = s &
T = t &
X = |[a,b]| &
w = ((- (2 * |((t - s),(s - |[a,b]|))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - |[a,b]|))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) &
s <> t &
s in inside_of_circle (
a,
b,
r) holds
ex
e being
Point of
(TOP-REAL 2) st
(
{e} = (halfline (s,t)) /\ (circle (a,b,r)) &
e = ((1 - w) * s) + (w * t) )
theorem
for
a,
b,
r being
Real for
s,
t being
Point of
(TOP-REAL 2) st
s in circle (
a,
b,
r) &
t in inside_of_circle (
a,
b,
r) holds
(LSeg (s,t)) /\ (circle (a,b,r)) = {s}
theorem
for
a,
b,
r being
Real for
s,
t being
Point of
(TOP-REAL 2) st
s in circle (
a,
b,
r) &
t in circle (
a,
b,
r) holds
(LSeg (s,t)) \ {s,t} c= inside_of_circle (
a,
b,
r)
theorem
for
a,
b,
r being
Real for
s,
t being
Point of
(TOP-REAL 2) st
s in circle (
a,
b,
r) &
t in circle (
a,
b,
r) holds
(LSeg (s,t)) /\ (circle (a,b,r)) = {s,t}
theorem
for
a,
b,
r being
Real for
s,
t being
Point of
(TOP-REAL 2) st
s in circle (
a,
b,
r) &
t in circle (
a,
b,
r) holds
(halfline (s,t)) /\ (circle (a,b,r)) = {s,t}
theorem
for
a,
b,
r,
w being
Real for
s,
t being
Point of
(TOP-REAL 2) for
S,
T,
Y being
Element of
REAL 2 st
S = ((1 / 2) * s) + ((1 / 2) * t) &
T = t &
Y = |[a,b]| &
s <> t &
s in circle (
a,
b,
r) &
t in closed_inside_of_circle (
a,
b,
r) holds
ex
e being
Point of
(TOP-REAL 2) st
(
e <> s &
{s,e} = (halfline (s,t)) /\ (circle (a,b,r)) & (
t in Sphere (
|[a,b]|,
r) implies
e = t ) & ( not
t in Sphere (
|[a,b]|,
r) &
w = ((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies
e = ((1 - w) * (((1 / 2) * s) + ((1 / 2) * t))) + (w * t) ) )