{"id":"palomar/PALOMAR-2026-09-25-000007","url":"https://github.com/bjbraams/lean-LCS/tree/d2a9c3112132820d7d1bf2fbc340a9db3cd6213a","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-25-000007-v1.json","repo":"https://github.com/bjbraams/lean-LCS","tags":["math.FA","msc:46A03","msc:46A08","msc:46A30","msc:46A20","msc:46A25","msc:46A13","msc:46A04","functional-analysis","locally-convex-spaces"],"score":0,"title":"lean-LCS: locally convex spaces, duality, and closed graph theorems in Lean 4","trust":"high","domain":"math.FA","source":"palomar","authors":["Bastiaan J. Braams"],"reviews":0,"subject":"math.FA","summary":"A Lean 4 formalization, built on Mathlib, of the basic theory of locally convex topological vector spaces over the real or complex numbers. It covers barrelled, quasi-barrelled, bornological and ultrabornological spaces; the closed graph and open mapping theorems for barrelled spaces, and Pták's closed graph and open mapping theorems; duality theory with the bipolar, Alaoglu–Bourbaki, Mackey, Mackey–Arens, Banach–Dieudonné and Krein–Šmulian theorems and Grothendieck's completeness theorem; semi-reflexive, reflexive and Montel spaces with their permanence properties; completeness of strong…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-25","reactions":{},"formalized":true,"formalizes":[{"title":"Topological Vector Spaces (second edition)","identifier":"doi:10.1007/978-1-4612-1468-7","relationship":"formalizes"},{"title":"Topological Vector Spaces I","identifier":"doi:10.1007/978-3-642-64988-2","relationship":"formalizes"},{"title":"Topological Vector Spaces II","identifier":"doi:10.1007/978-1-4684-9409-9","relationship":"formalizes"},{"title":"Topological Vector Spaces, Chapters 1–5","identifier":"doi:10.1007/978-3-642-61715-7","relationship":"formalizes"}]}