Commit 2026-06-11 01:51 b657502d

View on Github →

feat: Analytic Hahn Banach theorem for locally convex spaces (#38739) Closes #38419 This PR proves Hahn-Banach theorem for locally convex spaces, which allow us to generalize both ContinuousLinearMap.exist_extension_of_finiteDimensional_range and Submodule.ClosedComplemented.of_finiteDimensional (I also moved these two lemmas to the new file I created). Some helper lemmas about continuity of seminorms/linear functions are added. Created with the help of Codex.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/LocallyConvex/HahnBanach.lean

added theorem ContinuousLinearMap.exist_extension_of_finiteDimensional_range

added theorem Module.Dual.exists_continuous_extension_of_le_seminorm

added theorem Module.Dual.exists_continuous_extension_of_le_seminorm_real

added theorem Module.Dual.exists_extension_of_le_seminorm

added theorem Module.Dual.exists_extension_of_le_seminorm_real

added theorem StrongDual.exists_extension

added theorem Submodule.ClosedComplemented.of_finiteDimensional

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

added theorem Seminorm.abs_le_of_le

added theorem Seminorm.bound_comp_of_isInducing

added theorem Seminorm.exists_le_comp_of_isInducing

added theorem SeminormFamily.comp_smul_nnreal

added theorem WithSeminorms.continuous_real_rng

Modified Mathlib/Analysis/Normed/Module/HahnBanach.lean

deleted theorem ContinuousLinearMap.exist_extension_of_finiteDimensional_range

deleted theorem Real.exists_extension_norm_eq

deleted theorem Submodule.ClosedComplemented.of_finiteDimensional

Modified Mathlib/Analysis/Normed/Module/RCLike/Extend.lean

added theorem Module.Dual.norm_extendRCLike_le_seminorm

added theorem StrongDual.norm_extendRCLike_le_seminorm

Modified Mathlib/Analysis/Seminorm.lean

added theorem Seminorm.continuous_finsetSum

added theorem Seminorm.continuous_finsetSup