Summary
- Urysohn's lemma, Dugundji extension theorem and many other proofs
The file was added | src/HOL/Multivariate_Analysis/Extension.thy |
The file was modified | src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy (diff) |
The file was modified | src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy (diff) |
The file was modified | src/HOL/Multivariate_Analysis/Integration.thy (diff) |
The file was modified | src/HOL/Multivariate_Analysis/Path_Connected.thy (diff) |
The file was modified | src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy (diff) |