equal
deleted
inserted
replaced
98 |
98 |
99 |
99 |
100 subsection \<open>Continuity\<close> |
100 subsection \<open>Continuity\<close> |
101 |
101 |
102 lemma NSLIM_isContc_iff: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S f a \<longleftrightarrow> (\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S f a" |
102 lemma NSLIM_isContc_iff: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S f a \<longleftrightarrow> (\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S f a" |
103 by (rule NSLIM_h_iff) |
103 by (rule NSLIM_at0_iff) |
104 |
104 |
105 |
105 |
106 subsection \<open>Functions from Complex to Reals\<close> |
106 subsection \<open>Functions from Complex to Reals\<close> |
107 |
107 |
108 lemma isNSContCR_cmod [simp]: "isNSCont cmod a" |
108 lemma isNSContCR_cmod [simp]: "isNSCont cmod a" |