A Lean 4/mathlib project formalizing Schauder bases and unconditional Schauder bases for Banach spaces.
analysis mathematics proof-assistant lean formalization functional-analysis mathlib lean4 mathematical-proof formalized-mathematics formalised-mathematics schauder-basis
-
Updated
May 23, 2026 - Lean