hahn_banach thm file

mkerjean · mkerjean · commit 162230aebea0 · 2026-03-06T15:14:31.000+09:00
diff --git a/_CoqProject b/_CoqProject
@@ -87,6 +87,8 @@ theories/normedtype_theory/urysohn.v
 theories/normedtype_theory/vitali_lemma.v
 theories/normedtype_theory/normedtype.v
 
+theories/hahn_banach_theorem.v
+
 theories/sequences.v
 theories/realfun.v
 theories/exp.v
diff --git a/theories/Make b/theories/Make
@@ -53,6 +53,8 @@ normedtype_theory/urysohn.v
 normedtype_theory/vitali_lemma.v
 normedtype_theory/normedtype.v
 
+hahn_banach_theorem.v
+
 realfun.v
 sequences.v
 exp.v
diff --git a/theories/hahn_banach_theorem.v b/theories/hahn_banach_theorem.v
