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:
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 09 2023 at 02:02 UTC