From f9dd8a75aab0df385bb20af6f325362ba9493918 Mon Sep 17 00:00:00 2001 From: zstone Date: Mon, 11 Nov 2024 00:03:16 -0500 Subject: [PATCH] removing redundant name term --- CHANGELOG_UNRELEASED.md | 2 +- theories/function_spaces.v | 8 ++------ 2 files changed, 3 insertions(+), 7 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 653ebaa12..821c85866 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -97,7 +97,7 @@ - in file `weak_topology.v`, + new lemma `continuous_comp_weak`. - in file `function_spaces.v`, - + new definitions `eval`, and `comp_cts`. + + new definitions `eval`. + new lemmas `continuous_curry_fun`, `continuous_curry_joint_cvg`, `eval_continuous`, and `compose_continuous`. diff --git a/theories/function_spaces.v b/theories/function_spaces.v index 90b89f2d0..6ede30aa1 100644 --- a/theories/function_spaces.v +++ b/theories/function_spaces.v @@ -71,7 +71,6 @@ From mathcomp Require Import reals signed topology separation_axioms. (* {compact_open, U -> V} == compact-open topology *) (* {compact_open, F --> f} == F converges to f in {compact_open, U -> V} *) (* eval == the evaluation map for continuous functions *) -(* comp_cts == composition for continuous functions *) (* ``` *) (* *) (* ## Ascoli's theorem notations *) @@ -1561,10 +1560,6 @@ End currying. Definition eval {X Y : topologicalType} : continuousType X Y * X -> Y := uncurry (id : continuousType X Y -> (X -> Y)). -Definition comp_cts {X Y Z : topologicalType} (g : continuousType Y Z) - (f : continuousType X Y) : continuousType X Z := - g \o f. - Section composition. Local Import ArrowAsCompactOpen. @@ -1580,7 +1575,8 @@ Qed. Lemma compose_continuous {X Y Z : topologicalType} : locally_compact [set: X] -> @regular_space X -> locally_compact [set: Y] -> @regular_space Y -> - continuous (uncurry (@comp_cts X Y Z)). + continuous (uncurry + (comp : continuousType Y Z -> continuousType X Y -> continuousType X Z)). Proof. move=> ? ? lY rY; apply: continuous_comp_weak. set F := _ \o _.