src/HOL/Analysis/Cartesian_Euclidean_Space.thy
 changeset 69508 2a4c8a2a3f8e parent 69272 15e9ed5b28fb child 69597 ff784d5a5bfb
```     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed Dec 26 20:57:23 2018 +0100
1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Dec 27 19:48:28 2018 +0100
1.3 @@ -651,7 +651,7 @@
1.4
1.5  lemma%unimportant Lim_component_eq_cart:
1.6    fixes f :: "'a \<Rightarrow> real^'n"
1.7 -  assumes net: "(f \<longlongrightarrow> l) net" "~(trivial_limit net)" and ev:"eventually (\<lambda>x. f(x)\$i = b) net"
1.8 +  assumes net: "(f \<longlongrightarrow> l) net" "\<not> trivial_limit net" and ev:"eventually (\<lambda>x. f(x)\$i = b) net"
1.9    shows "l\$i = b"
1.10    using ev[unfolded order_eq_iff eventually_conj_iff] and
1.11      Lim_component_ge_cart[OF net, of b i] and
1.12 @@ -1060,7 +1060,7 @@
1.13
1.14  lemma%unimportant matrix_nonfull_linear_equations_eq:
1.15    fixes A :: "real^'n^'m"
1.16 -  shows "(\<exists>x. (x \<noteq> 0) \<and> A *v x = 0) \<longleftrightarrow> ~(rank A = CARD('n))"
1.17 +  shows "(\<exists>x. (x \<noteq> 0) \<and> A *v x = 0) \<longleftrightarrow> rank A \<noteq> CARD('n)"
1.18    by (meson matrix_left_invertible_injective full_rank_injective matrix_left_invertible_ker)
1.19
1.20  lemma%unimportant rank_eq_0: "rank A = 0 \<longleftrightarrow> A = 0" and rank_0 [simp]: "rank (0::real^'n^'m) = 0"
```