Commit 599c70e1 authored by Ralf Jung's avatar Ralf Jung
Browse files

a little theory about limit preservation

parent a09a8247
......@@ -959,6 +959,21 @@ Qed.
Class LimitPreserving `{!Cofe A} (P : A Prop) : Prop :=
limit_preserving : c : chain A, ( n, P (c n)) P (compl c).
Section limit_preserving.
Context {A : ofeT} `{!Cofe A}.
(* These are not instances as they will never fire automatically...
but they can still be helpful in proving things to be limit preserving. *)
Lemma limit_preserving_and (P1 P2 : A Prop) :
LimitPreserving P1 LimitPreserving P2
LimitPreserving (λ x, P1 x P2 x).
intros Hlim1 Hlim2 c Hc. split.
- apply Hlim1, Hc.
- apply Hlim2, Hc.
End limit_preserving.
Section sigma.
Context {A : ofeT} {P : A Prop}.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment