Skip to content

Commit

Permalink
fixes #1253
Browse files Browse the repository at this point in the history
  • Loading branch information
affeldt-aist committed Jun 27, 2024
1 parent 84cf8a3 commit f1c6761
Showing 1 changed file with 2 additions and 4 deletions.
6 changes: 2 additions & 4 deletions theories/function_spaces.v
Original file line number Diff line number Diff line change
Expand Up @@ -159,7 +159,6 @@ rewrite eqEsubset; split => y //; exists (dfwith (fun=> point) i y) => //.
by rewrite dfwithin.
Qed.


Lemma dfwith_continuous g (i : I) : continuous (@dfwith I K g i).
Proof.
move=> z U [] P [] [] Q QfinP <- [] V JV Vpz.
Expand Down Expand Up @@ -404,7 +403,7 @@ End product_spaces.

(**md the uniform topologies type *)
Section fct_Uniform.
Variable (T : choiceType) (U : uniformType).
Variables (T : choiceType) (U : uniformType).

Definition fct_ent := filter_from (@entourage U)
(fun P => [set fg | forall t : T, P (fg.1 t, fg.2 t)]).
Expand Down Expand Up @@ -444,7 +443,6 @@ Definition arrow_uniform_type : Type := T -> U.
#[export] HB.instance Definition _ := isUniform.Build arrow_uniform_type
fct_ent_filter fct_ent_refl fct_ent_inv fct_ent_split.

#[export] HB.instance Definition _ := Uniform.on arrow_uniform_type.
End fct_Uniform.

Lemma cvg_fct_entourageP (T : choiceType) (U : uniformType)
Expand Down Expand Up @@ -580,7 +578,7 @@ Notation "{ 'uniform' , F --> f }" :=
(cvg_to F (nbhs (f : {uniform _ -> _}))) : classical_set_scope.

Definition sigL_arrow {U : choiceType} (A : set U) (V : uniformType) :
(U -> V) -> arrow_uniform_type A V := (@sigL _ V A).
(U -> V) -> arrow_uniform_type A V := @sigL _ V A.

HB.instance Definition _ (U : choiceType) (A : set U) (V : uniformType) :=
Uniform.copy {uniform` A -> V} (weak_topology (@sigL_arrow _ A V)).
Expand Down

0 comments on commit f1c6761

Please sign in to comment.