% A partial order on R induces a partial order on functions that range in R,
% called the pointwise order. The pointwise order preserves complete
% lower semilattices, complete upper semilattices, and complete lattices.
%
% Author: Alfons Geser ([email protected]), National Institute of Aerospace
% Date: Dec 2004
pointwise_orders[
D, R: TYPE
]: THEORY
BEGIN
IMPORTING bounded_orders, skolemization[D, R], closure_ops
x: VAR D
r, s: VAR R
rr: VAR set[R]
f, g: VAR [D -> R]
ff: VAR set[[D -> R]]
nff: VAR non_empty_finite_set[[D -> R]]
rel: VAR pred[[R,R]]
alt: VAR (antisymmetric?[R])
% f is pointwise less than, or equal to, g if f(x) <= g(x) for all x.
pointwise(rel)(f,g): bool = FORALL x: rel(f(x), g(x))
strictly_pointwise(rel): pred[[[D -> R], [D -> R]]] =
irreflexive_kernel(pointwise(reflexive_closure(rel)))
pointwise_preserves_reflexive: JUDGEMENT
pointwise(rel: (reflexive?[R])) HAS_TYPE (reflexive?[[D -> R]])
pointwise_preserves_transitive: JUDGEMENT
pointwise(rel: (transitive?[R])) HAS_TYPE (transitive?[[D -> R]])
pointwise_preserves_preorder: JUDGEMENT
pointwise(lt: (preorder?[R])) HAS_TYPE (preorder?[[D -> R]])
pointwise_preserves_antisymmetric: JUDGEMENT
pointwise(rel: (antisymmetric?[R])) HAS_TYPE (antisymmetric?[[D -> R]])
pointwise_preserves_partial_order: JUDGEMENT
pointwise(lt: (partial_order?[R])) HAS_TYPE (partial_order?[[D -> R]])
% if nff is non-empty and finite, then so is every set of the form
% {s | EXISTS f: nff(f) & s = f(x)} for any x
finiteness_lemma: LEMMA
nonempty?[R]({s | EXISTS f: nff(f) & s = f(x)}) AND
is_finite[R]({s | EXISTS f: nff(f) & s = f(x)})
least_upper_bound_pointwise: THEOREM
least_upper_bound?[[D -> R]](f, ff, pointwise(rel)) IFF
FORALL x:
least_upper_bound?[R](f(x), {s | EXISTS f: ff(f) AND s = f(x)}, rel)
least_bounded_above_pointwise: LEMMA
least_bounded_above?[[D -> R]](ff, pointwise(rel)) IFF
FORALL x:
least_bounded_above?[R]({s | EXISTS f: ff(f) AND s = f(x)}, rel)
pointwise_preserves_upper_semilattices: JUDGEMENT
pointwise(lt: (upper_semilattice?[R])) HAS_TYPE
(upper_semilattice?[[D -> R]])
pointwise_preserves_complete_upper_semilattices: JUDGEMENT
pointwise(lt: (complete_upper_semilattice?[R])) HAS_TYPE
(complete_upper_semilattice?[[D -> R]])
greatest_lower_bound_pointwise: LEMMA
greatest_lower_bound?[[D -> R]](f, ff, pointwise(rel)) IFF
FORALL x:
greatest_lower_bound?[R](f(x), {s | EXISTS f: ff(f) & s = f(x)}, rel)
greatest_bounded_below_pointwise: LEMMA
greatest_bounded_below?(ff, pointwise(alt)) IFF
(FORALL x:
greatest_bounded_below?(alt)({s | EXISTS f: ff(f) & s = f(x)}))
pointwise_preserves_lower_semilattices: JUDGEMENT
pointwise(lt: (lower_semilattice?[R])) HAS_TYPE
(lower_semilattice?[[D -> R]])
pointwise_preserves_complete_lower_semilattices: JUDGEMENT
pointwise(lt: (complete_lower_semilattice?[R])) HAS_TYPE
(complete_lower_semilattice?[[D -> R]])
pointwise_preserves_lattices: JUDGEMENT
pointwise(lt: (lattice?[R])) HAS_TYPE (lattice?[[D -> R]])
pointwise_preserves_complete_lattices: JUDGEMENT
pointwise(lt: (complete_lattice?[R])) HAS_TYPE
(complete_lattice?[[D -> R]])
lub_pointwise_def: LEMMA
(FORALL x:
least_bounded_above?(alt)({s | EXISTS f: ff(f) & s = f(x)})) =>
lub[[D -> R]](pointwise(alt))(ff) =
LAMBDA x: lub[R](alt)({s | EXISTS f: ff(f) & s = f(x)})
glb_pointwise_def: LEMMA
(FORALL x:
greatest_bounded_below?(alt)({s | EXISTS f: ff(f) & s = f(x)})) =>
glb[[D -> R]](pointwise(alt))(ff) =
LAMBDA x: glb[R](alt)({s | EXISTS f: ff(f) & s = f(x)})
END pointwise_orders
¤ Dauer der Verarbeitung: 0.13 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.
|
