Library ZFstable
Require Import ZFsum ZFpairs ZFrelations ZFnats ZFord ZFfix.
Lemma cst_is_ext : ∀ X o, ext_fun o (fun _ => X).
Hint Resolve cst_is_ext.
Lemma sum_is_ext : ∀ o F G,
ext_fun o F ->
ext_fun o G ->
ext_fun o (fun y => sum (F y) (G y)).
Hint Resolve sum_is_ext.
Lemma func_is_ext : ∀ x X F,
ext_fun x F ->
ext_fun x (fun x => func X (F x)).
Hint Resolve func_is_ext.
Lemma increasing_is_ext : ∀ F,
increasing F ->
∀ o, isOrd o ->
ext_fun o F.
Hint Resolve increasing_is_ext.
Stable functions
Definition stable2 F :=
∀ X Y, F X ∩ F Y ⊆ F (X ∩ Y).
Definition stable F :=
∀ X,
inter (replf X F) ⊆ F (inter X).
Lemma stable2_weaker :
∀ F, morph1 F -> stable F -> stable2 F.
Library of stable operators
Lemma cst_stable : ∀ A, stable (fun _ => A).
Lemma id_stable : stable (fun x => x).
Lemma power_stable : stable power.
Lemma prodcart_stable : ∀ F G,
morph1 F ->
morph1 G ->
stable F ->
stable G ->
stable (fun y => prodcart (F y) (G y)).
Lemma sigma_stable' : ∀ A F,
(∀ y y' x x', y == y' -> x ∈ A -> x == x' -> F y x == F y' x') ->
(∀ x, x ∈ A -> stable (fun y => F y x)) ->
stable (fun y => sigma A (F y)).
Lemma sigma_stable : ∀ F G,
morph1 F ->
morph2 G ->
stable F ->
(∀ x, stable (fun y => G y x)) ->
stable (fun y => sigma (F y) (G y)).
Lemma sum_stable : ∀ F G,
morph1 F ->
morph1 G ->
stable F ->
stable G ->
stable (fun y => sum (F y) (G y)).
Lemma func_stable : ∀ A,
stable (func A).
Lemma cc_prod_stable : ∀ dom F,
(∀ y y' x x', y == y' -> x ∈ dom -> x == x' -> F y x == F y' x') ->
(∀ x, x ∈ dom -> stable (fun y => F y x)) ->
stable (fun y => cc_prod dom (F y)).
Lemma id_stable : stable (fun x => x).
Lemma power_stable : stable power.
Lemma prodcart_stable : ∀ F G,
morph1 F ->
morph1 G ->
stable F ->
stable G ->
stable (fun y => prodcart (F y) (G y)).
Lemma sigma_stable' : ∀ A F,
(∀ y y' x x', y == y' -> x ∈ A -> x == x' -> F y x == F y' x') ->
(∀ x, x ∈ A -> stable (fun y => F y x)) ->
stable (fun y => sigma A (F y)).
Lemma sigma_stable : ∀ F G,
morph1 F ->
morph2 G ->
stable F ->
(∀ x, stable (fun y => G y x)) ->
stable (fun y => sigma (F y) (G y)).
Lemma sum_stable : ∀ F G,
morph1 F ->
morph1 G ->
stable F ->
stable G ->
stable (fun y => sum (F y) (G y)).
Lemma func_stable : ∀ A,
stable (func A).
Lemma cc_prod_stable : ∀ dom F,
(∀ y y' x x', y == y' -> x ∈ dom -> x == x' -> F y x == F y' x') ->
(∀ x, x ∈ dom -> stable (fun y => F y x)) ->
stable (fun y => cc_prod dom (F y)).
Stability of ordinal-indexed families
Definition stable2_ord F :=
∀ x, isOrd x ->
∀ y, isOrd y ->
F x ∩ F y ⊆ F (x ∩ y).
Definition stable_ord F :=
∀ X,
(∀ x, x ∈ X -> isOrd x) ->
inter (replf X F) ⊆ F (inter X).
Lemma compose_stable : ∀ F G,
Proper (incl_set ==> incl_set) F ->
morph1 G ->
stable F ->
stable_ord G ->
stable_ord (fun o => F (G o)).
Lemma TI_stable2 : ∀ F,
Proper (incl_set ==> incl_set) F ->
stable2 F ->
stable2_ord (TI F).
Lemma TI_stable : ∀ F,
Proper (incl_set ==> incl_set) F ->
stable F ->
stable_ord (TI F).