Library ZFfunext
Building a function by compatible union of functions
Definition fcompat dom f g :=
∀ x, x ∈ dom -> cc_app f x == cc_app g x.
Instance fext_morph :
Proper (eq_set ==> eq_set ==> eq_set ==> iff) fcompat.
Qed.
Lemma fext_lam : ∀ A B f g,
ext_fun A f ->
ext_fun B g ->
(∀ x, x ∈ A -> x ∈ B) ->
(∀ x, x ∈ A -> f x == g x) ->
fcompat A (cc_lam A f) (cc_lam B g).
Lemma fcompat_typ_eq : ∀ A f f',
is_cc_fun A f ->
is_cc_fun A f' ->
fcompat A f f' ->
f == f'.
Section ExtendFamily.
Variable I : set.
Variable A F : set -> set.
Hypothesis extA : ext_fun I A.
Hypothesis extF : ext_fun I F.
Hypothesis in_prod : ∀ x, x ∈ I -> is_cc_fun (A x) (F x).
Definition fdirected :=
∀ x y, x ∈ I -> y ∈ I -> fcompat (A x ∩ A y) (F x) (F y).
Hypothesis fcomp : fdirected.
Lemma fdir :
∀ x0 x1 x z,
x0 ∈ I ->
x1 ∈ I ->
x ∈ A x0 ->
z ∈ cc_app (F x1) x ->
z ∈ cc_app (F x0) x.
Lemma prd_union : is_cc_fun (sup I A) (sup I F).
Lemma prd_sup : ∀ x,
x ∈ I ->
fcompat (A x) (F x) (sup I F).
Lemma prd_sup_lub : ∀ g,
(∀ x, x ∈ I -> fcompat (A x) (F x) g) ->
fcompat (sup I A) (sup I F) g.
End ExtendFamily.