Hello, how can I write the statement "sqrtr is continuous" in an environment where reals, topology, normedtype, landau, and derive from mathcomp.analysis have been loaded?

I tried writing the following:

```
Lemma sqrt_continuous : continuous (@Num.sqrt R).```
but I get a phantom error message which seems to indicate that my type is not located correctly in the hierarchy.
```

Would this be good enough?

```
From mathcomp Require Import all_ssreflect ssralg ssrnum.
Require Import boolp reals classical_sets topology.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import numFieldTopology.Exports.
Lemma sqrt_continuous (R : realType) : continuous (@Num.sqrt R).
Abort.
Require Import Reals Rstruct.
Lemma sqrt_continuous : continuous (@Num.sqrt [rcfType of R]).
Abort.
```

Thanks, the difficulty for me was that Require Import ... topology is not enough, I also need the line you included:

```
Import numFieldTopology.Exports.
```

I will keep experimenting.

This topic was moved here from #math-comp users > Getting started with mathcomp-analysis : continuo... by Cyril Cohen

Last updated: Feb 22 2024 at 03:02 UTC