Commit 2023-11-16 06:00 8a954749

View on Github →

chore: split Analysis.Convex.Cone.Basic (#8357) Splits Mathlib.Analysis.Convex.Cone.Basic, to move Riesz extension and Hahn-Banach out of the basic file about definitions.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Convex/Cone/Basic.lean

deleted theorem RieszExtension.exists_top

deleted theorem RieszExtension.step

deleted theorem exists_extension_of_le_sublinear

deleted theorem riesz_extension

Modified Mathlib/Analysis/Convex/Cone/Dual.lean

Created Mathlib/Analysis/Convex/Cone/Extension.lean

added theorem RieszExtension.exists_top

added theorem RieszExtension.step

added theorem exists_extension_of_le_sublinear

added theorem riesz_extension

Modified Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean

Modified Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean