environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, ALGSTR_0, SUBSET_1, ARYTM_1, IDEAL_1, ARYTM_3, FUNCSDOM, STRUCT_0, TARSKI, MESFUNC1, SUPINF_2, BINOP_1, FUNCT_1, RELAT_1, RLVECT_1, VECTSP_1, RSSPACE, GROUP_1, REAL_1, POLYALG1, CARD_1, FUNCOP_1, FUNCT_2, VALUED_1, LOPBAN_1, COMPLEX1, XXREAL_0, PRE_TOPC, NAT_1, C0SP1, FINSEQ_1, FINSEQ_2, RCOMP_1, PARTFUN1, ORDINAL4, FDIFF_1, PDIFF_1, REAL_NS1, EUCLID, CFCONT_1, RFINSEQ, CARD_3, PDIFF_9, CKSPACE1, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_1, COMPLEX1, FINSEQ_1, VALUED_1, FINSEQ_2, RFINSEQ, SEQFUNC, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, GROUP_1, VECTSP_1, FUNCSDOM, EUCLID, LOPBAN_1, IDEAL_1, C0SP1, NFCONT_1, NDIFF_1, REAL_NS1, PDIFF_1, PDIFF_6, PDIFF_7, PDIFF_9;
definitions TARSKI;
theorems FUNCT_1, COMPLEX1, ZFMISC_1, TARSKI, XREAL_0, XXREAL_0, FUNCSDOM, LOPBAN_1, FUNCT_2, XREAL_1, RLVECT_1, FUNCOP_1, VALUED_1, IDEAL_1, RELSET_1, XBOOLE_1, EUCLID, FINSEQ_1, FINSEQ_2, FINSEQ_3, RFINSEQ, NAT_1, FINSEQ_5, PARTFUN1, NDIFF_1, REAL_NS1, PDIFF_1, ORDINAL1, PDIFF_6, PDIFF_7, INT_1, PDIFF_9, C0SP1;
schemes NAT_1;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, NUMBERS, ORDINAL1, MEMBERED, FUNCSDOM, VECTSP_1, VECTSP_2, VALUED_0, RELSET_1, NAT_1, FINSEQ_1, EUCLID, REAL_NS1, FUNCT_2, XREAL_0;
constructors HIDDEN, REAL_1, REALSET1, MEASURE6, BINOP_2, SEQ_1, IDEAL_1, XXREAL_2, RELSET_1, SQUARE_1, NFCONT_1, FDIFF_1, NDIFF_1, PDIFF_1, MONOID_0, INTEGR15, RFINSEQ, NAT_D, PDIFF_6, VFUNCT_1, PDIFF_7, VALUED_2, NFCONT_4, SEQFUNC, PDIFF_9, C0SP1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities ALGSTR_0, FINSEQ_1, FUNCSDOM, RLVECT_1, STRUCT_0, BINOP_1, VALUED_1, PDIFF_9;
expansions TARSKI, RLVECT_1, PDIFF_9;
Lm1:
for m being non zero Element of NAT
for I being non empty FinSequence of NAT
for i being Element of NAT st rng I c= Seg m & i <= (len I) - 1 holds
( 1 <= I /. (i + 1) & I /. (i + 1) <= m )
Lm2:
for m being non zero Element of NAT
for I being non empty FinSequence of NAT
for i being Element of NAT st rng I c= Seg m & 1 <= i & i <= len I holds
( 1 <= I /. i & I /. i <= m )
definition
let m be non
zero Element of
NAT ;
let k be
Element of
NAT ;
let X be non
empty open Subset of
(REAL m);
func R_Algebra_of_Ck_Functions (
k,
X)
-> Subalgebra of
RAlgebra X equals
AlgebraStr(#
(Ck_Functions (k,X)),
(mult_ ((Ck_Functions (k,X)),(RAlgebra X))),
(Add_ ((Ck_Functions (k,X)),(RAlgebra X))),
(Mult_ ((Ck_Functions (k,X)),(RAlgebra X))),
(One_ ((Ck_Functions (k,X)),(RAlgebra X))),
(Zero_ ((Ck_Functions (k,X)),(RAlgebra X))) #);
coherence
AlgebraStr(# (Ck_Functions (k,X)),(mult_ ((Ck_Functions (k,X)),(RAlgebra X))),(Add_ ((Ck_Functions (k,X)),(RAlgebra X))),(Mult_ ((Ck_Functions (k,X)),(RAlgebra X))),(One_ ((Ck_Functions (k,X)),(RAlgebra X))),(Zero_ ((Ck_Functions (k,X)),(RAlgebra X))) #) is Subalgebra of RAlgebra X
by C0SP1:6;
end;
::
deftheorem defines
R_Algebra_of_Ck_Functions CKSPACE1:def 3 :
for m being non zero Element of NAT
for k being Element of NAT
for X being non empty open Subset of (REAL m) holds R_Algebra_of_Ck_Functions (k,X) = AlgebraStr(# (Ck_Functions (k,X)),(mult_ ((Ck_Functions (k,X)),(RAlgebra X))),(Add_ ((Ck_Functions (k,X)),(RAlgebra X))),(Mult_ ((Ck_Functions (k,X)),(RAlgebra X))),(One_ ((Ck_Functions (k,X)),(RAlgebra X))),(Zero_ ((Ck_Functions (k,X)),(RAlgebra X))) #);
registration
let m be non
zero Element of
NAT ;
let k be
Element of
NAT ;
let X be non
empty open Subset of
(REAL m);
coherence
( R_Algebra_of_Ck_Functions (k,X) is Abelian & R_Algebra_of_Ck_Functions (k,X) is add-associative & R_Algebra_of_Ck_Functions (k,X) is right_zeroed & R_Algebra_of_Ck_Functions (k,X) is right_complementable & R_Algebra_of_Ck_Functions (k,X) is vector-distributive & R_Algebra_of_Ck_Functions (k,X) is scalar-distributive & R_Algebra_of_Ck_Functions (k,X) is scalar-associative & R_Algebra_of_Ck_Functions (k,X) is scalar-unital & R_Algebra_of_Ck_Functions (k,X) is commutative & R_Algebra_of_Ck_Functions (k,X) is associative & R_Algebra_of_Ck_Functions (k,X) is right_unital & R_Algebra_of_Ck_Functions (k,X) is right-distributive & R_Algebra_of_Ck_Functions (k,X) is scalar-associative & R_Algebra_of_Ck_Functions (k,X) is vector-associative )
end;