|
deriv_domain: THEORY
BEGIN
a,b: VAR real
IMPORTING deriv_domain_def
deriv_domain_real : LEMMA deriv_domain?[real]
deriv_domain_nzreal : LEMMA deriv_domain?[nzreal]
deriv_domain_posreal: LEMMA deriv_domain?[posreal]
deriv_domain_nnreal : LEMMA deriv_domain?[nnreal]
deriv_domain_negreal: LEMMA deriv_domain?[negreal]
IMPORTING reals@intervals_real
deriv_domain_open : LEMMA deriv_domain?[open_interval(a,b)]
deriv_domain_closed : LEMMA a /= b IMPLIES deriv_domain?[closed_interval(a,b)]
deriv_domain_oc : LEMMA deriv_domain?[{x: real | a < x AND x <= b}]
deriv_domain_co : LEMMA deriv_domain?[{x: real | a <= x AND x < b}]
deriv_domain_posreal_le: LEMMA deriv_domain?[{x: posreal | x <= a}]
deriv_domain_posreal_lt: LEMMA deriv_domain?[{x: posreal | x < a}]
deriv_domain_nnreal_lt : LEMMA deriv_domain?[{x: nnreal | x < a}]
% ------- Not One Element Lemmas
not_one_element_real : LEMMA not_one_element?[real]
not_one_element_nzreal : LEMMA not_one_element?[nzreal]
not_one_element_posreal: LEMMA not_one_element?[posreal]
not_one_element_nnreal : LEMMA not_one_element?[nnreal]
not_one_element_negreal: LEMMA not_one_element?[negreal]
% ------- Connected Lemmas
connected_real : LEMMA connected?[real]
connected_posreal: LEMMA connected?[posreal]
connected_nnreal : LEMMA connected?[nnreal]
connected_negreal: LEMMA not_one_element?[negreal]
END deriv_domain
¤ Dauer der Verarbeitung: 0.16 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.
|
