summaryrefslogtreecommitdiff
path: root/theories/Reals/Rsqrt_def.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Reals/Rsqrt_def.v')
-rw-r--r--theories/Reals/Rsqrt_def.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index 6a3dd976..9b8dd1db 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -392,7 +392,7 @@ Definition cond_positivity (x:R) : bool :=
| right _ => false
end.
-(** Sequential caracterisation of continuity *)
+(** Sequential characterisation of continuity *)
Lemma continuity_seq :
forall (f:R -> R) (Un:nat -> R) (l:R),
continuity_pt f l -> Un_cv Un l -> Un_cv (fun i:nat => f (Un i)) (f l).