Library ZFlimit
Building the limit of a sequence of sets
Variable o : set.
Variable F : set -> set.
Hypothesis oord : isOrd o.
Hypothesis Fm : ext_fun o F.
Definition lim :=
subset (sup o F) (fun z => exists2 o', o' ∈ o & ∀ w, o' ⊆ w -> w ∈ o -> z ∈ F w).
Lemma lim_def z :
z ∈ lim <-> exists2 o', o' ∈ o &∀ w, o' ⊆ w -> w ∈ o -> z ∈ F w.
Variable F : set -> set.
Hypothesis oord : isOrd o.
Hypothesis Fm : ext_fun o F.
Definition lim :=
subset (sup o F) (fun z => exists2 o', o' ∈ o & ∀ w, o' ⊆ w -> w ∈ o -> z ∈ F w).
Lemma lim_def z :
z ∈ lim <-> exists2 o', o' ∈ o &∀ w, o' ⊆ w -> w ∈ o -> z ∈ F w.
If the sequence is stationary, it has a limit
Limits at a successor ordinal is just the last value
Lemma lim_oucc o F :
isOrd o ->
ext_fun (osucc o) F ->
lim (osucc o) F == F o.
Lemma lim_ext :
∀ o o', isOrd o -> o == o' -> ∀ f f', eq_fun o f f' -> lim o f == lim o' f'.
Instance lim_morph : Proper (eq_set==>(eq_set==>eq_set)==>eq_set) lim.
Qed.
isOrd o ->
ext_fun (osucc o) F ->
lim (osucc o) F == F o.
Lemma lim_ext :
∀ o o', isOrd o -> o == o' -> ∀ f f', eq_fun o f f' -> lim o f == lim o' f'.
Instance lim_morph : Proper (eq_set==>(eq_set==>eq_set)==>eq_set) lim.
Qed.
Limits of a monotonic operator
Section LimitMono.
Variable F:set->set.
Variable o : set.
Hypothesis oord : isOrd o.
Hypothesis Fmono : increasing F.
Let os := fun y => isOrd_inv _ y oord.
Let Fext : ext_fun o F.
Qed.
Variable F:set->set.
Variable o : set.
Hypothesis oord : isOrd o.
Hypothesis Fmono : increasing F.
Let os := fun y => isOrd_inv _ y oord.
Let Fext : ext_fun o F.
Qed.
This is the same as the union
Lemma lim_def_mono : lim o F == sup o F.
Lemma lim_mono z :
z ∈ lim o F <-> exists2 o', o' ∈ o & z ∈ F o'.
End LimitMono.
Lemma lim_mono z :
z ∈ lim o F <-> exists2 o', o' ∈ o & z ∈ F o'.
End LimitMono.
Limit of the transfinite iteration
Section LimitTI.
Variable F : set->set.
Hypothesis Fm : Proper (incl_set==>incl_set) F.
Lemma TIlim o :
isOrd o ->
TI F o == lim o (fun o' => F(TI F o')).
End LimitTI.
Section TRF.
Hypothesis F:(set->set->set)->set->set->set.
Hypothesis Fext : ∀ o o' f f' x x',
isOrd o ->
(∀ o' o'' x x', o' ∈ o -> o'==o'' -> x==x' -> f o' x == f' o'' x') ->
o == o' ->
x == x' ->
F f o x == F f' o' x'.
Fixpoint TR_acc (o:set) (H:Acc in_set o) (H':isOrd o) (x:set) : set :=
F (fun o' x' => ZFrepl.uchoice (fun y' => exists h:o' ∈ o, y' == TR_acc o' (Acc_inv H h) (isOrd_inv _ _ H' h) x')) o x.
Lemma TR_acc_morph o o' h h' oo oo' x x' :
o == o' ->
x == x' ->
TR_acc o h oo x == TR_acc o' h' oo' x'.
Lemma isOrd_acc o : isOrd o -> Acc in_set o.
Definition TR o x := ZFrepl.uchoice (fun y => exists h:isOrd o, y == TR_acc o (isOrd_acc _ h) h x).
Lemma TR_acc_eqn o h h' x :
TR_acc o h h' x == F TR o x.
Lemma TR_eqn o x :
isOrd o ->
TR o x == F TR o x.
Global Instance TR_morph : morph2 TR.
Qed.
End TRF.
Section TR_irrel.
Variable F : (set->set->set)->set->set->set.
Variable T : set -> set.
Variable Tcont : ∀ o z, isOrd o ->
(z ∈ T o <-> exists2 o', o' ∈ o & z ∈ T (osucc o')).
Hypothesis Fext : ∀ o o' f f' x x',
isOrd o ->
(∀ o' o'' x x', o' ∈ o -> o'==o'' -> x==x' -> f o' x == f' o'' x') ->
o == o' ->
x == x' ->
F f o x == F f' o' x'.
Hypothesis Firr : ∀ o o' f f' x x',
morph2 f ->
morph2 f' ->
isOrd o ->
isOrd o' ->
(∀ o1 o1' x x',
o1 ∈ o -> o1' ∈ o' -> o1 ⊆ o1' -> x ∈ T o1 -> x==x' ->
f o1 x == f' o1' x') ->
o ⊆ o' ->
x ∈ T o ->
x == x' ->
F f o x == F f' o' x'.
Lemma TR_irrel : ∀ o o' x,
isOrd o ->
isOrd o' ->
o' ⊆ o ->
x ∈ T o' ->
TR F o x == TR F o' x.
End TR_irrel.
Section TRirr.
Variable F : (set->set)->set->set.
Hypothesis Fm : Proper ((eq_set==>eq_set)==>eq_set==>eq_set) F.
Variable T : set -> set.
Variable Tcont : ∀ o z, isOrd o ->
(z ∈ T o <-> exists2 o', o' ∈ o & z ∈ T (osucc o')).
Hypothesis Fext : ∀ o f f',
isOrd o ->
eq_fun (T o) f f' ->
eq_fun (T (osucc o)) (F f) (F f').
Lemma Tmono o o': isOrd o -> isOrd o' -> o ⊆ o' -> T o ⊆ T o'.
Let G f o x := F (fun x => lim o (fun o' => f o' x)) x.
Definition TRF := TR G.
Let Gext : ∀ o o' f f' x x',
isOrd o ->
(∀ o' o'' x x', o' ∈ o -> o'==o'' -> x==x' -> f o' x == f' o'' x') ->
o == o' ->
x == x' ->
G f o x == G f' o' x'.
Qed.
Let Girr : ∀ o o' f f' x x',
morph2 f ->
morph2 f' ->
isOrd o ->
isOrd o' ->
(∀ o1 o1' x x',
o1 ∈ o -> o1' ∈ o' -> o1 ⊆ o1' -> x ∈ T o1 -> x==x' ->
f o1 x == f' o1' x') ->
o ⊆ o' ->
x ∈ T o ->
x == x' ->
G f o x == G f' o' x'.
Qed.
Instance TRF_morph : morph2 TRF.
Qed.
Lemma TRF_indep : ∀ o o' x,
isOrd o ->
o' ∈ o ->
x ∈ T (osucc o') ->
TRF o x == F (TRF o') x.
End TRirr.
Variable F : set->set.
Hypothesis Fm : Proper (incl_set==>incl_set) F.
Lemma TIlim o :
isOrd o ->
TI F o == lim o (fun o' => F(TI F o')).
End LimitTI.
Section TRF.
Hypothesis F:(set->set->set)->set->set->set.
Hypothesis Fext : ∀ o o' f f' x x',
isOrd o ->
(∀ o' o'' x x', o' ∈ o -> o'==o'' -> x==x' -> f o' x == f' o'' x') ->
o == o' ->
x == x' ->
F f o x == F f' o' x'.
Fixpoint TR_acc (o:set) (H:Acc in_set o) (H':isOrd o) (x:set) : set :=
F (fun o' x' => ZFrepl.uchoice (fun y' => exists h:o' ∈ o, y' == TR_acc o' (Acc_inv H h) (isOrd_inv _ _ H' h) x')) o x.
Lemma TR_acc_morph o o' h h' oo oo' x x' :
o == o' ->
x == x' ->
TR_acc o h oo x == TR_acc o' h' oo' x'.
Lemma isOrd_acc o : isOrd o -> Acc in_set o.
Definition TR o x := ZFrepl.uchoice (fun y => exists h:isOrd o, y == TR_acc o (isOrd_acc _ h) h x).
Lemma TR_acc_eqn o h h' x :
TR_acc o h h' x == F TR o x.
Lemma TR_eqn o x :
isOrd o ->
TR o x == F TR o x.
Global Instance TR_morph : morph2 TR.
Qed.
End TRF.
Section TR_irrel.
Variable F : (set->set->set)->set->set->set.
Variable T : set -> set.
Variable Tcont : ∀ o z, isOrd o ->
(z ∈ T o <-> exists2 o', o' ∈ o & z ∈ T (osucc o')).
Hypothesis Fext : ∀ o o' f f' x x',
isOrd o ->
(∀ o' o'' x x', o' ∈ o -> o'==o'' -> x==x' -> f o' x == f' o'' x') ->
o == o' ->
x == x' ->
F f o x == F f' o' x'.
Hypothesis Firr : ∀ o o' f f' x x',
morph2 f ->
morph2 f' ->
isOrd o ->
isOrd o' ->
(∀ o1 o1' x x',
o1 ∈ o -> o1' ∈ o' -> o1 ⊆ o1' -> x ∈ T o1 -> x==x' ->
f o1 x == f' o1' x') ->
o ⊆ o' ->
x ∈ T o ->
x == x' ->
F f o x == F f' o' x'.
Lemma TR_irrel : ∀ o o' x,
isOrd o ->
isOrd o' ->
o' ⊆ o ->
x ∈ T o' ->
TR F o x == TR F o' x.
End TR_irrel.
Section TRirr.
Variable F : (set->set)->set->set.
Hypothesis Fm : Proper ((eq_set==>eq_set)==>eq_set==>eq_set) F.
Variable T : set -> set.
Variable Tcont : ∀ o z, isOrd o ->
(z ∈ T o <-> exists2 o', o' ∈ o & z ∈ T (osucc o')).
Hypothesis Fext : ∀ o f f',
isOrd o ->
eq_fun (T o) f f' ->
eq_fun (T (osucc o)) (F f) (F f').
Lemma Tmono o o': isOrd o -> isOrd o' -> o ⊆ o' -> T o ⊆ T o'.
Let G f o x := F (fun x => lim o (fun o' => f o' x)) x.
Definition TRF := TR G.
Let Gext : ∀ o o' f f' x x',
isOrd o ->
(∀ o' o'' x x', o' ∈ o -> o'==o'' -> x==x' -> f o' x == f' o'' x') ->
o == o' ->
x == x' ->
G f o x == G f' o' x'.
Qed.
Let Girr : ∀ o o' f f' x x',
morph2 f ->
morph2 f' ->
isOrd o ->
isOrd o' ->
(∀ o1 o1' x x',
o1 ∈ o -> o1' ∈ o' -> o1 ⊆ o1' -> x ∈ T o1 -> x==x' ->
f o1 x == f' o1' x') ->
o ⊆ o' ->
x ∈ T o ->
x == x' ->
G f o x == G f' o' x'.
Qed.
Instance TRF_morph : morph2 TRF.
Qed.
Lemma TRF_indep : ∀ o o' x,
isOrd o ->
o' ∈ o ->
x ∈ T (osucc o') ->
TRF o x == F (TRF o') x.
End TRirr.