src/HOL/Library/Euclidean_Space.thy
changeset 30655 88131f2807b6
parent 30582 638b088bb840
child 30665 4cf38ea4fad2
equal deleted inserted replaced
30654:254478a8dd05 30655:88131f2807b6
     3 *)
     3 *)
     4 
     4 
     5 header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*}
     5 header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*}
     6 
     6 
     7 theory Euclidean_Space
     7 theory Euclidean_Space
     8   imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Complex_Main
     8 imports Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
     9   Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type
     9   Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type
    10   Inner_Product
    10   Inner_Product
    11   uses ("normarith.ML")
    11 uses ("normarith.ML")
    12 begin
    12 begin
    13 
    13 
    14 text{* Some common special cases.*}
    14 text{* Some common special cases.*}
    15 
    15 
    16 lemma forall_1: "(\<forall>i::1. P i) \<longleftrightarrow> P 1"
    16 lemma forall_1: "(\<forall>i::1. P i) \<longleftrightarrow> P 1"