Library ZFcont

Require Export basic.
Require Import ZF ZFpairs ZFsum ZFfix ZFnats ZFord ZFstable ZFrank ZFrelations.
Import ZFrepl.

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.

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)).