|
step_fun_scaf[T: TYPE+ FROM real]: THEORY
BEGIN
ASSUMING
IMPORTING deriv_domain_def[T]
connected_domain : ASSUMPTION connected?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
% AUTO_REWRITE+ not_one_element
IMPORTING integral_step, partitions_scaf[T]
a,b,c,d,x,y,z: VAR T
f,f1,f2,g: VAR [T -> real]
eps, delta: VAR posreal
xv,yv: VAR real
UP_prep: LEMMA FORALL (a:T, b: {x:T|a<x}, P1,P2: partition[T](a, b)):
LET UP = union[T](part2set(a,b,P1), part2set(a,b,P2)) IN
card(UP) > 1
AND UP(a) AND UP(b)
UnionPart(a:T,b:{x:T|a<x},P1,P2: partition[T](a,b)): partition[T](a,b) =
set2part(union(part2set(a, b, P1), part2set(a, b, P2)))
UnionPart_lem: LEMMA FORALL (a:T, b: {x:T|a<x}, P1,P2: partition[T](a, b),
kk: below(length(P1)-1)):
EXISTS (nn: below(length(UnionPart(a,b,P1,P2)))):
UnionPart(a,b,P1,P2)`seq(nn) = P1`seq(kk)
Union_sym: LEMMA FORALL (a:T, b: {x:T|a<x}, P1,P2: partition[T](a, b)):
UnionPart(a,b,P1,P2) = UnionPart(a,b,P2,P1)
Union_lem: LEMMA FORALL (a:T, b: {x:T|a<x}, P1,P2: partition[T](a, b),
nn: below(length(UnionPart(a,b,P1,P2))-1)):
in_sect?(a,b,UnionPart(a,b,P1,P2),nn,x)
IMPLIES
(EXISTS (kk: below(length(P1)-1)):
seq(P1)(kk) <= UnionPart(a,b,P1,P2)(nn) AND
UnionPart(a,b,P1,P2)(nn+1) <= seq(P1)(kk+1) )
END step_fun_scaf
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
