Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 16.11.2025 mit Größe 33 kB

Quellcode-Bibliothek 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%

¤ 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.0.0Bemerkung: (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.