Quelle continuity_interval.pvs Sprache: PVS

continuity_interval [ a : real, b : {x : real | a <= x }] : THEORY
%-----------------------------------------------------------------
%  continuous functions on a closed interval
%-----------------------------------------------------------------
BEGIN

  %-----------------------------
  %  Interval [a, b] as a type
  %-----------------------------

  x : VAR real
  J : NONEMPTY_TYPE = { x | a <= x AND x <= b}
  f : VAR [J -> real]
  u : VAR sequence[J]
  c : VAR J
  n, i : VAR nat

  IMPORTING continuity_props

  %-----------------------------------------------
  %  Reformulation of Bolzano/Weirstrass theorem
  %-----------------------------------------------

  bolz_weier : LEMMA   EXISTS c : accumulation(u, c)

  %-------------------------------------
  %  If f is continuous, it is bounded
  %-------------------------------------

  unbounded_sequence : LEMMA bounded_above?(f) OR
                               EXISTS u : FORALL n : f(u(n)) > n

  bounded_from_above : LEMMA continuous?(f) IMPLIES bounded_above?(f)

  bounded_from_below : LEMMA continuous?(f) IMPLIES bounded_below?(f)

  %--------------------------------------
  %  f has a maximum and a minimum in J
  %--------------------------------------

  max_extraction : LEMMA continuous?(f) IMPLIES
                    EXISTS u : FORALL n : sup(f) - f(u(n)) < 1/(n+1)

  sup_is_reached : LEMMA continuous?(f) IMPLIES EXISTS c : f(c) = sup(f)

  maximum_exists : LEMMA continuous?(f) IMPLIES EXISTS c : is_maximum(c, f)

  max_pt(f:{f|continuous?(f)}): {xj: J | is_maximum(xj,f)}     % ADDED BY RWB

  inf_is_reached : LEMMA continuous?(f) IMPLIES EXISTS c : f(c) = inf(f)

  minimum_exists : LEMMA continuous?(f) IMPLIES EXISTS c : is_minimum(c, f)

  min_pt(f:{f|continuous?(f)}): {xj: J | is_minimum(xj,f)}     % ADDED BY RWB

  %-------------------------------
  %  Intermediate value theorem
  %-------------------------------

  intermediate_value1 : LEMMA continuous?(f) AND f(a) < x AND x < f(b)
                         IMPLIES EXISTS c : f(c) = x

  intermediate_value2 : LEMMA continuous?(f) AND f(a) <= x AND x <= f(b)
                         IMPLIES EXISTS c : f(c) = x

  intermediate_value3 : LEMMA continuous?(f) AND f(b) < x AND x < f(a)
                         IMPLIES EXISTS c : f(c) = x

  intermediate_value4 : LEMMA continuous?(f) AND f(b) <= x AND x <= f(a)
                         IMPLIES EXISTS c : f(c) = x

END continuity_interval

quality93%

¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.