isabelle: src/HOL/Analysis/Multivariate_Analysis.thy@7e2a9a8c2b85 (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	wenzelm
	Sat, 20 Feb 2021 13:42:37 +0100
changeset 73255	7e2a9a8c2b85
parent 71027	b212ee44f87c
permissions	-rw-r--r--