environ
vocabularies HIDDEN, XREAL_0, VALUED_1, INT_1, NEWTON, MEMBERED, PARTFUN1, RCOMP_3, TOPMETR, SEQ_4, INTEGRA1, MEASURE7, COUSIN, NORMSP_2, SETFAM_1, RELAT_1, COMPL_SP, PROB_1, FUNCT_2, NUMBERS, SUBSET_1, NAT_1, FUNCT_1, ARYTM_3, FINSEQ_2, ZFMISC_1, COMPLEX1, STRUCT_0, XBOOLE_0, NORMSP_1, EUCLID, PRE_TOPC, REAL_1, CARD_1, XXREAL_0, ARYTM_1, FINSEQ_1, CARD_3, ORDINAL4, TARSKI, SQUARE_1, SEQ_2, ORDINAL2, SEQ_1, RSSPACE3, REWRITE1, METRIC_1, BHSP_3, REAL_NS1, NORMSP_0, XXREAL_2, XXREAL_1, MEASURE5, RCOMP_1, PCOMPS_1, POWER, RFINSEQ, RELAT_2, PARTFUN3, VALUED_0;
notations HIDDEN, INT_1, NEWTON, VALUED_1, MEMBERED, PARTFUN1, CONNSP_1, SETFAM_1, TOPS_2, TOPMETR, XXREAL_2, RELAT_1, FUNCT_1, XBOOLE_0, TARSKI, XCMPLX_0, XXREAL_0, FINSEQ_1, RFINSEQ, METRIC_1, ZFMISC_1, SUBSET_1, BINOP_1, PRE_TOPC, NAT_1, FINSEQ_2, FUNCT_2, STRUCT_0, NUMBERS, XREAL_0, SQUARE_1, COMPLEX1, RLVECT_1, SEQ_1, SEQ_2, RVSUM_1, NORMSP_0, NORMSP_1, RSSPACE3, REAL_NS1, TBSP_1, EUCLID, PROB_1, KURATO_0, RELSET_1, PCOMPS_1, CARD_3, KURATO_2, NORMSP_2, COMPL_SP, RCOMP_1, MEASURE5, SEQ_4, INTEGRA1, SEQM_3, PARTFUN3, RCOMP_3, MATRPROB, POWER;
definitions TARSKI;
theorems CGAMES_1, NUMBERS, FUNCT_6, BORSUK_4, NAT_6, VALUED_1, PROB_1, TOPREAL6, NEWTON, XXREAL_2, JORDAN6, PRE_TOPC, TOPS_2, SETFAM_1, TOPMETR, RCOMP_3, XTUPLE_0, PARTFUN1, VALUED_0, JORDAN5A, INTEGRA1, SRINGS_4, TOPREALC, METRIC_1, COMPL_SP, XXREAL_1, EUCLID, BINOP_1, ABSVALUE, RSSPACE3, FINSEQ_1, FINSEQ_2, FUNCT_2, LOPBAN_1, NAT_1, SQUARE_1, FUNCT_1, FINSEQ_5, XREAL_1, XXREAL_0, ORDINAL1, TBSP_1, REAL_NS1, XBOOLE_0, TARSKI, PCOMPS_1, XBOOLE_1, CARD_3, UNIFORM1, NORMSP_2, JORDAN2B, RFINSEQ, FINSEQ_3, XCMPLX_1, INT_1, MEASURE5, SEQ_4, PARTFUN3, SEQ_1, SEQ_2, TOPREAL3, POWER, MEMBERED;
schemes NAT_1, FUNCT_2, XBOOLE_0;
registrations SEQ_2, LOPBAN_5, VALUED_1, XXREAL_2, METRIC_1, MATRTOP1, BORSUK_5, JORDAN5A, COMPLEX1, SUBSET_1, FUNCT_1, RELSET_1, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, VALUED_0, FUNCT_2, EUCLID, FINSEQ_1, CARD_1, NAT_1, REAL_NS1, COMPL_SP, MEASURE5, INTEGRA1, SEQM_3, RELAT_1, ORDINAL1, XCMPLX_0, NUMBERS, INT_1, RVSUM_1, SEQ_4, PARTFUN3, POWER;
constructors HIDDEN, NEWTON, CONNSP_1, TOPS_2, RCOMP_3, SQUARE_1, RSSPACE3, LOPBAN_1, RVSUM_1, COMSEQ_2, REAL_NS1, TBSP_1, KURATO_0, COMPL_SP, FRECHET, NORMSP_2, SEQ_4, INTEGRA1, MEASURE6, RFINSEQ, REAL_1, PARTFUN3, MATRPROB, POWER;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities NORMSP_0, SUBSET_1, METRIC_1, XBOOLE_0;
expansions FUNCT_1, NORMSP_1, STRUCT_0, TARSKI, TBSP_1, METRIC_1, XBOOLE_0, SEQM_3;
theorem Th2:
for
a,
b being
Real st 1
< a & 1
< b holds
0 < log (
a,
b)
theorem Th8:
for
a,
b being
Real st
a <= b holds
(
a <= (a + b) / 2 &
(a + b) / 2
<= b )
theorem
for
a,
b,
c being
Real st
a <= b &
b < c holds
a < (b + c) / 2
theorem
for
a,
b being
Real st
a < b holds
(a + b) / 2
< b
theorem
for
r being
Real for
a,
b being
Real_Sequence st
0 < r &
a . 0 <= b . 0 & ( for
i being
Nat holds
( (
a . (i + 1) = a . i &
b . (i + 1) = ((a . i) + (b . i)) / 2 ) or (
a . (i + 1) = ((a . i) + (b . i)) / 2 &
b . (i + 1) = b . i ) ) ) holds
ex
c being
Real st
( ( for
j being
Nat holds
(
a . j <= c &
c <= b . j ) ) & ex
k being
Nat st
(
c - r < a . k &
b . k < c + r ) )
theorem
for
r,
s being
Real for
jauge being
Function of
[.r,s.],
].0,+infty.[ for
S being
Subset-Family of
(Closed-Interval-TSpace (r,s)) st
r <= s &
S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } holds
for
IC being
IntervalCover of
S holds
(
IC is
FinSequence of
bool REAL &
rng IC c= S &
union (rng IC) = [.r,s.] & ( for
n being
Nat st 1
<= n holds
( (
n <= len IC implies not
IC /. n is
empty ) & (
n + 1
<= len IC implies (
lower_bound (IC /. n) <= lower_bound (IC /. (n + 1)) &
upper_bound (IC /. n) <= upper_bound (IC /. (n + 1)) &
lower_bound (IC /. (n + 1)) < upper_bound (IC /. n) ) ) & (
n + 2
<= len IC implies
upper_bound (IC /. n) <= lower_bound (IC /. (n + 2)) ) ) ) & (
[.r,s.] in S implies
IC = <*[.r,s.]*> ) & ( not
[.r,s.] in S implies ( ex
p being
Real st
(
r < p &
p <= s &
IC . 1
= [.r,p.[ ) & ex
p being
Real st
(
r <= p &
p < s &
IC . (len IC) = ].p,s.] ) & ( for
n being
Nat st 1
< n &
n < len IC holds
ex
p,
q being
Real st
(
r <= p &
p < q &
q <= s &
IC . n = ].p,q.[ ) ) ) ) )
theorem Th42:
for
r,
s,
t,
x being
Real holds
( (
r <= x - t &
x + t <= s implies
].(x - t),(x + t).[ /\ [.r,s.] = ].(x - t),(x + t).[ ) & (
r <= x - t &
s < x + t implies
].(x - t),(x + t).[ /\ [.r,s.] = ].(x - t),s.] ) & (
x - t < r &
x + t <= s implies
].(x - t),(x + t).[ /\ [.r,s.] = [.r,(x + t).[ ) & (
x - t < r &
s < x + t implies
].(x - t),(x + t).[ /\ [.r,s.] = [.r,s.] ) )