Library ZFcont
Require Export basic.
Require Import ZF ZFpairs ZFsum ZFfix ZFnats ZFord ZFstable ZFrank ZFrelations.
Import ZFrepl.
Require Import ZF ZFpairs ZFsum ZFfix ZFnats ZFord ZFstable ZFrank ZFrelations.
Import ZFrepl.
Geeralized continuity
Definition continuous o F :=
∀ X, ext_fun o X -> F (sup o X) == sup o (fun z => F (X z)).
Section Convergence.
Variable o :set.
Hypothesis oo : limitOrd o.
Hypothesis F : set->set.
Hypothesis Fm : morph1 F.
Hypothesis Fcont : continuous o F.
Lemma Fcont_mono :
(exists x, x ∈ o) -> Proper (incl_set==>incl_set) F.
Lemma cont_least_fix : F (TI F o) == TI F o.
End Convergence.
A small libary of continuous functions
Lemma cst_cont : ∀ X o, (exists y, lt y o) -> X == sup o (fun _ => X).
Lemma sum_cont : ∀ o F G,
ext_fun o F ->
ext_fun o G ->
sum (sup o F) (sup o G) == sup o (fun y => sum (F y) (G y)).
Lemma sup_cont : ∀ o F G,
ext_fun o F ->
ext_fun o G ->
sup o F ∪ sup o G == sup o (fun y => F y ∪ G y).
Lemma sigma_cont dom A f :
morph2 f ->
sigma A (fun x => sup dom (f x)) == sup dom (fun i => sigma A (fun x => f x i)).
Section ProductContinuity.
Hypothesis mu : set.
Hypothesis mu_ord : isOrd mu.
Variable X : set.
Hypothesis X_small : bound_ord X mu.
Lemma func_cont_gen : ∀ F,
stable_ord F ->
increasing F ->
func X (sup mu F) ⊆ sup mu (fun A => func X (F A)).
Hypothesis mu_bound : lt (osup (func X mu) (fun f => osup X (app f))) mu.
Lemma func_bound : bound_ord X mu.
End ProductContinuity.
Lemma func_cont : ∀ mu X F,
isOrd mu ->
VN_regular mu ->
omega ∈ mu ->
stable_ord F ->
increasing F ->
X ∈ VN mu ->
func X (sup mu F) == sup mu (fun x => func X (F x)).