environ
vocabularies HIDDEN, NUMBERS, REAL_1, XBOOLE_0, RLVECT_1, SUBSET_1, PRE_TOPC, RELAT_1, XCMPLX_0, SETFAM_1, TARSKI, ALGSTR_0, ARYTM_3, ZFMISC_1, STRUCT_0, SUPINF_2, ARYTM_1, CONNSP_2, TOPS_1, CONVEX1, CARD_1, XXREAL_0, RELAT_2, COMPLEX1, BINOP_1, FUNCT_1, RCOMP_1, ORDINAL2, TOPS_2, YELLOW13, XXREAL_2, FINSET_1, RVSUM_1, EQREL_1, COMPTS_1, RLTOPSP1, FUNCT_2, INCSP_1, AFF_1, PENCIL_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, SETFAM_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, BINOP_1, REAL_1, EQREL_1, DOMAIN_1, STRUCT_0, ALGSTR_0, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_2, COMPTS_1, YELLOW13, RLVECT_1, RUSUB_4, CONVEX1;
definitions TARSKI, XBOOLE_0, STRUCT_0, RLVECT_1, PRE_TOPC, CONNSP_2, TOPS_2, YELLOW13, CONVEX1, ALGSTR_0, SETFAM_1, ZFMISC_1;
theorems TARSKI, XBOOLE_0, XBOOLE_1, ZFMISC_1, SUBSET_1, SETFAM_1, XCMPLX_1, XREAL_0, XCMPLX_0, FUNCT_2, FUNCT_1, ABSVALUE, FINSET_1, EQREL_1, PRE_TOPC, COMPTS_1, CONNSP_2, TOPS_1, URYSOHN1, YELLOW13, RLVECT_1, RUSUB_4, CONVEX1, TOPGRP_1, TOPS_2, YELLOW_8, XREAL_1, TSEP_1, COMPLEX1, XXREAL_0, XTUPLE_0, STRUCT_0;
schemes BINOP_1, FUNCT_2, SUBSET_1, EQREL_1, FINSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, PARTFUN1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, STRUCT_0, TOPS_1, RLVECT_1, CONVEX1, TOPGRP_1, ORDINAL1, BORSUK_1, COMPTS_1, PRE_TOPC, FUNCT_2, ANPROJ_1;
constructors HIDDEN, SETFAM_1, BINOP_1, DOMAIN_1, XXREAL_0, REAL_1, COMPLEX1, EQREL_1, TOPS_1, TOPS_2, CONNSP_2, RUSUB_4, CONVEX1, URYSOHN1, YELLOW13, COMPTS_1, RELSET_1, NUMBERS;
requirements HIDDEN, BOOLE, REAL, NUMERALS, SUBSET, ARITHM;
equalities STRUCT_0, RLVECT_1, CONVEX1, SUBSET_1, ALGSTR_0, XCMPLX_0;
expansions TARSKI, XBOOLE_0, PRE_TOPC, TOPS_2, CONVEX1;
reconsider jj = 1 as positive Real ;
Lm1:
for X being non empty addLoopStr
for M being Subset of X
for x, y being Point of X st y in M holds
x + y in x + M
Lm2:
for X being non empty addLoopStr
for M, N being Subset of X holds { (x + N) where x is Point of X : x in M } is Subset-Family of X
Lm3:
for X being non empty addLoopStr
for M, N, V being Subset of X st M c= N holds
V + M c= V + N
Lm4:
for X being RealLinearSpace holds conv ({} X) = {}
Lm5:
for X being RealLinearSpace
for A, B being circled Subset of X holds A + B is circled
Lm6:
for X being RealLinearSpace
for A being circled Subset of X holds A is symmetric
Lm7:
for X being RealLinearSpace
for M being circled Subset of X holds conv M is circled
Lm8:
for X being LinearTopSpace
for a being Point of X holds transl (a,X) is one-to-one
Lm9:
for X being LinearTopSpace
for a being Point of X holds transl (a,X) is continuous
Lm10:
for X being LinearTopSpace
for E being Subset of X
for x being Point of X st E is open holds
x + E is open
Lm11:
for X being LinearTopSpace
for E being open Subset of X
for K being Subset of X holds K + E is open
Lm12:
for X being LinearTopSpace
for D being closed Subset of X
for x being Point of X holds x + D is closed
Lm13:
for X being LinearTopSpace
for r being non zero Real holds mlt (r,X) is one-to-one
Lm14:
for X being LinearTopSpace
for r being non zero Real holds mlt (r,X) is continuous
Lm15:
for X being LinearTopSpace
for V being bounded Subset of X
for r being Real holds r * V is bounded
Lm16:
for X being LinearTopSpace
for C being convex Subset of X holds Cl C is convex
Lm17:
for X being LinearTopSpace
for C being convex Subset of X holds Int C is convex
Lm18:
for X being LinearTopSpace
for B being circled Subset of X holds Cl B is circled
Lm19:
for X being LinearTopSpace
for E being bounded Subset of X holds Cl E is bounded
Lm20:
for X being LinearTopSpace
for U, V being a_neighborhood of 0. X
for F being Subset-Family of X
for r being positive Real st ( for s being Real st |.s.| < r holds
s * V c= U ) & F = { (a * V) where a is Real : |.a.| < r } holds
( union F is a_neighborhood of 0. X & union F is circled & union F c= U )
theorem
for
V being
RealLinearSpace for
x1,
x2,
x3,
x4 being
Point of
V st
x1,
x2,
x3,
x4 are_collinear holds
(
x1,
x2,
x3 are_collinear &
x1,
x2,
x4 are_collinear ) ;
theorem
for
V being
RealLinearSpace for
x1,
x2,
x3,
x4 being
Point of
V st
x1 <> x2 &
x1,
x2,
x3 are_collinear &
x1,
x2,
x4 are_collinear holds
x1,
x2,
x3,
x4 are_collinear