Library ZFfixfun
Construction of a function (a.k.a a family of sets) over a fixed domain by
transfinite iteration. No fixpoint theorem here.
Order on families
Definition incl_fam A X Y :=
∀ a, a ∈ A -> X a ⊆ Y a.
Instance incl_fam_trans : ∀ A, Transitive (incl_fam A).
Qed.
∀ a, a ∈ A -> X a ⊆ Y a.
Instance incl_fam_trans : ∀ A, Transitive (incl_fam A).
Qed.
Monotonicity
Definition mono_fam A F :=
∀ X Y, morph1 X -> morph1 Y -> incl_fam A X Y -> incl_fam A (F X) (F Y).
Section IterMonotone.
Variable A : set.
Variable F : (set -> set) -> set -> set.
Variable Fm : Proper ((eq_set==>eq_set) ==> eq_set ==> eq_set) F.
Variable Fmono : mono_fam A F.
Lemma FFmono_ext: ∀ X Y, morph1 X -> morph1 Y -> eq_fun A X Y -> eq_fun A (F X) (F Y).
Hint Resolve FFmono_ext.
∀ X Y, morph1 X -> morph1 Y -> incl_fam A X Y -> incl_fam A (F X) (F Y).
Section IterMonotone.
Variable A : set.
Variable F : (set -> set) -> set -> set.
Variable Fm : Proper ((eq_set==>eq_set) ==> eq_set ==> eq_set) F.
Variable Fmono : mono_fam A F.
Lemma FFmono_ext: ∀ X Y, morph1 X -> morph1 Y -> eq_fun A X Y -> eq_fun A (F X) (F Y).
Hint Resolve FFmono_ext.
Definition of the TIF iterator
Let F' f o := cc_lam A (fun a => sup o (fun o' => F (cc_app (f o')) a)).
Let F'm : Proper ((eq_set==>eq_set)==>eq_set==>eq_set) F'.
Qed.
Let F'ext : ∀ o f f', isOrd o -> eq_fun o f f' -> F' f o == F' f' o.
Qed.
Definition TIF o := cc_app (TR F' o).
Instance TIF_morph : morph2 TIF.
Qed.
Let m2: ∀ a a' o o', a ∈ A -> a == a' -> isOrd o -> o == o' ->
F (TIF o) a == F (TIF o') a'.
Qed.
Lemma TIF_eq : ∀ o a,
isOrd o ->
a ∈ A ->
TIF o a == sup o (fun o' => F (TIF o') a).
Lemma TIF_intro : ∀ o o' a x,
isOrd o ->
lt o' o ->
a ∈ A ->
x ∈ F (TIF o') a ->
x ∈ TIF o a.
Lemma TIF_elim : ∀ o x a,
isOrd o ->
a ∈ A ->
x ∈ TIF o a ->
exists2 o', lt o' o & x ∈ F (TIF o') a.
Let F'm : Proper ((eq_set==>eq_set)==>eq_set==>eq_set) F'.
Qed.
Let F'ext : ∀ o f f', isOrd o -> eq_fun o f f' -> F' f o == F' f' o.
Qed.
Definition TIF o := cc_app (TR F' o).
Instance TIF_morph : morph2 TIF.
Qed.
Let m2: ∀ a a' o o', a ∈ A -> a == a' -> isOrd o -> o == o' ->
F (TIF o) a == F (TIF o') a'.
Qed.
Lemma TIF_eq : ∀ o a,
isOrd o ->
a ∈ A ->
TIF o a == sup o (fun o' => F (TIF o') a).
Lemma TIF_intro : ∀ o o' a x,
isOrd o ->
lt o' o ->
a ∈ A ->
x ∈ F (TIF o') a ->
x ∈ TIF o a.
Lemma TIF_elim : ∀ o x a,
isOrd o ->
a ∈ A ->
x ∈ TIF o a ->
exists2 o', lt o' o & x ∈ F (TIF o') a.
Monotonicity of TIF
Lemma TIF_mono : ∀ a, a ∈ A -> increasing (fun o => TIF o a).
Lemma TIF_incl : ∀ o, isOrd o ->
∀ o', lt o' o ->
∀ a, a ∈ A ->
TIF o' a ⊆ TIF o a.
Lemma TIF_mono_succ : ∀ o a,
isOrd o ->
a ∈ A ->
TIF (osucc o) a == F (TIF o) a.
Lemma TIF_mono_eq : ∀ o a,
isOrd o ->
a ∈ A ->
TIF o a == sup o (fun o' => TIF (osucc o') a).
Lemma TIF_incl : ∀ o, isOrd o ->
∀ o', lt o' o ->
∀ a, a ∈ A ->
TIF o' a ⊆ TIF o a.
Lemma TIF_mono_succ : ∀ o a,
isOrd o ->
a ∈ A ->
TIF (osucc o) a == F (TIF o) a.
Lemma TIF_mono_eq : ∀ o a,
isOrd o ->
a ∈ A ->
TIF o a == sup o (fun o' => TIF (osucc o') a).
Property related to fixpoints: any post-fixpoint fx contains all stages