isabelle: src/HOL/Analysis/Multivariate_Analysis.thy@b212ee44f87c (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	immler
	Mon, 04 Nov 2019 17:59:32 -0500
changeset 71027	b212ee44f87c
parent 70621	1afcfb7fdff4
permissions	-rw-r--r--