author nipkow Sun Jan 06 12:32:01 2019 +0100 (4 months ago) changeset 69600 86e8e7347ac0 parent 69599 caa7e406056d child 69606 157990515be1
typed definitions
 src/HOL/Analysis/Abstract_Topology.thy file | annotate | diff | revisions src/HOL/Analysis/Inner_Product.thy file | annotate | diff | revisions src/HOL/Analysis/L2_Norm.thy file | annotate | diff | revisions src/HOL/Analysis/Linear_Algebra.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Analysis/Abstract_Topology.thy	Sat Jan 05 20:12:02 2019 +0100
1.2 +++ b/src/HOL/Analysis/Abstract_Topology.thy	Sun Jan 06 12:32:01 2019 +0100
1.3 @@ -13,7 +13,8 @@
1.4
1.5  subsection \<open>General notion of a topology as a value\<close>
1.6
1.7 -definition%important "istopology L \<longleftrightarrow>
1.8 +definition%important istopology :: "('a set \<Rightarrow> bool) \<Rightarrow> bool" where
1.9 +"istopology L \<longleftrightarrow>
1.10    L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union>K))"
1.11
1.12  typedef%important 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
1.13 @@ -113,7 +114,8 @@
1.14
1.15  subsubsection \<open>Closed sets\<close>
1.16
1.17 -definition%important "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
1.18 +definition%important closedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> bool" where
1.19 +"closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
1.20
1.21  lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U"
1.22    by (metis closedin_def)
1.23 @@ -230,7 +232,8 @@
1.24
1.25  subsection \<open>Subspace topology\<close>
1.26
1.27 -definition%important "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
1.28 +definition%important subtopology :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a topology" where
1.29 +"subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
1.30
1.31  lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
1.32    (is "istopology ?L")
```
```     2.1 --- a/src/HOL/Analysis/Inner_Product.thy	Sat Jan 05 20:12:02 2019 +0100
2.2 +++ b/src/HOL/Analysis/Inner_Product.thy	Sun Jan 06 12:32:01 2019 +0100
2.3 @@ -2,7 +2,7 @@
2.4      Author:     Brian Huffman
2.5  *)
2.6
2.7 -section \<open>Inner Product Spaces and the Gradient Derivative\<close>
2.8 +section \<open>Inner Product Spaces and Gradient Derivative\<close>
2.9
2.10  theory Inner_Product
2.11  imports Complex_Main
```
```     3.1 --- a/src/HOL/Analysis/L2_Norm.thy	Sat Jan 05 20:12:02 2019 +0100
3.2 +++ b/src/HOL/Analysis/L2_Norm.thy	Sun Jan 06 12:32:01 2019 +0100
3.3 @@ -8,7 +8,8 @@
3.4  imports Complex_Main
3.5  begin
3.6
3.7 -definition %important "L2_set f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
3.8 +definition%important L2_set :: "('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> real" where
3.9 +"L2_set f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
3.10
3.11  lemma L2_set_cong:
3.12    "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
```
```     4.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Sat Jan 05 20:12:02 2019 +0100
4.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Sun Jan 06 12:32:01 2019 +0100
4.3 @@ -183,7 +183,9 @@
4.4
4.5  subsection \<open>Bilinear functions\<close>
4.6
4.7 -definition%important "bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
4.8 +definition%important
4.9 +bilinear :: "('a::real_vector \<Rightarrow> 'b::real_vector \<Rightarrow> 'c::real_vector) \<Rightarrow> bool" where
4.10 +"bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
4.11
4.12  lemma bilinear_ladd: "bilinear h \<Longrightarrow> h (x + y) z = h x z + h y z"
4.13    by (simp add: bilinear_def linear_iff)
4.14 @@ -239,7 +241,8 @@
4.15