isabelle: src/HOL/Analysis/Multivariate_Analysis.thy@740b23f1138a (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	paulson <lp15@cam.ac.uk>
	Mon, 03 Jul 2023 11:45:59 +0100
changeset 78248	740b23f1138a
parent 71027	b212ee44f87c
permissions	-rw-r--r--