|
open_sets[T: TYPE FROM real]: THEORY
BEGIN
AUTO_REWRITE+ member
x,y: VAR T
S,S1,S2: VAR set[T]
open_ball?(x,S): bool = (EXISTS (delta: posreal):
(FORALL y: abs(x-y) < delta IMPLIES S(y)))
r: VAR posreal
open_ball(x,r): set[T] = {y: T | abs(x-y) < r}
open_ball?_lem: LEMMA open_ball?(x,S) IFF
EXISTS r: subset?(open_ball(x,r),S)
open?(S): bool = FORALL (x: (S)): open_ball?(x,S)
open?_lem: LEMMA open?(S) AND S(x) IMPLIES open_ball?(x,S)
closed?(S): bool = open?(complement(S))
Open : TYPE = (open?) %% = {S: set[T] | open?(S)}
Closed: TYPE = (closed?) %% = {S: set[T] | closed?(S)}
IMPORTING reals@intervals_real[T]
above_intv(a:T)(x) : MACRO bool = x > a
below_intv(a:T)(x) : MACRO bool = x < a
a,b: VAR T
% Open_empty : LEMMA {x: Open_interval(a,a) | TRUE} = emptyset[T]
open_intv_open : LEMMA a < b IMPLIES open?(open_intv(a,b))
above_intv_open : LEMMA open?(above_intv(a))
below_intv_open : LEMMA open?(below_intv(a))
union_open : LEMMA open?(S1) AND open?(S2) IMPLIES
open?(union(S1,S2))
closed_intv_closed : LEMMA a < b IMPLIES closed?(closed_intv(a,b))
END open_sets
¤ Dauer der Verarbeitung: 0.7 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
