Adding domain restrictions and compact convergence

theories/classical_sets.v

@@ -1332,6 +1332,75 @@ Proof. exact: (xgetPN point). Qed.
 
 End PointedTheory.
 
+Definition patch {U: Type} {V} (dflt : U -> V) (A : set U) (f : U -> V) u :=
+  if u \in A then f u else dflt u.
+
+Reserved Notation "f \|_ D" (at level 10).
+Notation restrict := (patch (fun=> point)).
+Notation "f \|_ D" := (restrict D).
+
+Definition restrict_dep {U V} (A : set U) (f : U -> V)
+  (u : { x : U | x \in A }) : V := f (projT1 u).
+Arguments restrict_dep {U V} A.
+
+Definition extend_dep {U} {V : pointedType} {A : set U}
+    (f : {x | x \in A } -> V) (u : U) :=
+  if pselect (u \in A) is left w then f (exist _ u w) else point.
+
+Lemma restrict_depE T T' (B : set T) x (f : T -> T') (xB : B x) :
+  restrict_dep B f (exist _ x (mem_set xB)) = f x.
+Proof. done. Qed.
+Arguments restrict_depE {T T'} B x.
+
+Lemma fun_eq_inP {U V} (f g : U -> V) (A : set U) :
+  {in A, f =1 g} <-> restrict_dep A f = restrict_dep A g.
+Proof.
+split=> [eq_f_g | Rfg u uA].
+  by rewrite funeqE /restrict_dep => -[x]; apply: eq_f_g.
+rewrite (_ : f u = restrict_dep A f (exist _ u uA)) //.
+rewrite (_ : g u = restrict_dep A g (exist _ u uA)) //.
+by move: Rfg; rewrite funeqE; apply.
+Qed.
+
+Section Restrictions.
+Context {U : Type} {V : pointedType} (A : set U).
+
+Local Notation extend_dep := (@extend_dep U V A).
+Local Notation restrict_dep := (@restrict_dep U V A).
+Local Notation restrict := (restrict A).
+
+Open Scope fun_scope.
+
+Lemma extend_restrict_dep : extend_dep \o restrict_dep = restrict.
+Proof.
+rewrite funeq2E => f u /=; rewrite /restrict_dep /restrict /extend_dep /patch.
+by case: pselect => [/= ->//|/negP/negbTE ->].
+Qed.
+
+Lemma extend_depK : cancel extend_dep restrict_dep.
+Proof.
+move=> f; rewrite funeqE => -[x /= xA].
+rewrite /restrict /patch /extend_dep /restrict_dep /=.
+by case: pselect => // xA'; congr (f (exist _ _ _)); apply: Prop_irrelevance.
+Qed.
+
+Lemma restrict_extend_dep : restrict_dep \o extend_dep = id.
+Proof. exact/funext/extend_depK. Qed.
+
+Lemma restrict_dep_restrict : restrict_dep \o restrict = restrict_dep.
+Proof.
+rewrite funeq2E => f -[u Au] /=.
+by rewrite /restrict_dep /restrict /extend_dep /patch /= Au.
+Qed.
+
+Lemma restrict_dep_setT : [set of restrict_dep] = setT.
+Proof.
+rewrite eqEsubset; split=> //= f _; exists (extend_dep f)=>//.
+exact: extend_depK.
+Qed.
+
+End Restrictions.
+
 Section partitions.
 
 Definition trivIset T I (D : set I) (F : I -> set T) :=