Theorem ContinuousLinearMap.exist_extension_of_finiteDimensional_range

Modification history

2026-06-11 01:51
Mathlib/Analysis/LocallyConvex/HahnBanach.lean
feat: Analytic Hahn Banach theorem for locally convex spaces (#38739) …
Modified ContinuousLinearMap.exist_extension_of_finiteDimensional_rangeView on Github →
2023-12-03 09:54
Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean
feat(Analysis/HahnBanach): extension of a CLM with finite dimensional range (#8604) …
Added ContinuousLinearMap.exist_extension_of_finiteDimensional_rangeView on Github →