isabelle: src/HOL/Analysis/Multivariate_Analysis.thy@d804e93ae9ff (annotated)

70621 1afcfb7fdff4 entry point for analysis without integration theory immler parents: diff changeset	1	theory
1afcfb7fdff4 entry point for analysis without integration theory immler parents: diff changeset	2	Multivariate_Analysis
1afcfb7fdff4 entry point for analysis without integration theory immler parents: diff changeset	3	imports
1afcfb7fdff4 entry point for analysis without integration theory immler parents: diff changeset	4	Ordered_Euclidean_Space
1afcfb7fdff4 entry point for analysis without integration theory immler parents: diff changeset	5	Determinants
1afcfb7fdff4 entry point for analysis without integration theory immler parents: diff changeset	6	Cross3
1afcfb7fdff4 entry point for analysis without integration theory immler parents: diff changeset	7	Lipschitz
71027 b212ee44f87c the division between Starlike and Convex_Euclidean_Space is artificial, therefore include Starlike immler parents: 70621 diff changeset	8	Starlike
70621 1afcfb7fdff4 entry point for analysis without integration theory immler parents: diff changeset	9	begin
1afcfb7fdff4 entry point for analysis without integration theory immler parents: diff changeset	10
1afcfb7fdff4 entry point for analysis without integration theory immler parents: diff changeset	11	text \<open>Entry point excluding integration and complex analysis.\<close>
1afcfb7fdff4 entry point for analysis without integration theory immler parents: diff changeset	12
1afcfb7fdff4 entry point for analysis without integration theory immler parents: diff changeset	13	end

author	haftmann
	Mon, 02 Aug 2021 10:01:06 +0000
changeset 74101	d804e93ae9ff
parent 71027	b212ee44f87c
permissions	-rw-r--r--