isabelle: src/HOL/Analysis/Multivariate_Analysis.thy@1ac2416e8432 (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
	Mon, 24 Oct 2022 20:37:32 +0200
changeset 76371	1ac2416e8432
parent 71027	b212ee44f87c
permissions	-rw-r--r--