Skip to content

Commit ebcdbc0

Browse files
committed
copy hahn banach from old branch, does not compile yet
1 parent 8df0315 commit ebcdbc0

4 files changed

Lines changed: 1114 additions & 8 deletions

File tree

_CoqProject

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -132,6 +132,8 @@ theories/kernel.v
132132
theories/pi_irrational.v
133133
theories/gauss_integral.v
134134

135+
theories/hahn_banach_theorem.v
136+
135137
theories/all_analysis.v
136138

137139
theories/showcase/summability.v

theories/Make

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -94,6 +94,9 @@ ftc.v
9494
hoelder.v
9595
probability.v
9696
convex.v
97+
98+
hahn_banach_theorem.v
99+
97100
charge.v
98101
kernel.v
99102
pi_irrational.v

0 commit comments

Comments
 (0)