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"