Skip to content

Commit 3b9685c

Browse files
committed
copy hahn banach from old branch
- use convex.v - does not compile yet
1 parent b9d779d commit 3b9685c

5 files changed

Lines changed: 1157 additions & 34 deletions

File tree

_CoqProject

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -143,6 +143,8 @@ theories/kernel.v
143143
theories/pi_irrational.v
144144
theories/gauss_integral.v
145145

146+
theories/hahn_banach_theorem.v
147+
146148
theories/all_analysis.v
147149

148150
theories/showcase/summability.v

theories/Make

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -104,6 +104,9 @@ probability_theory/beta_distribution.v
104104
probability_theory/probability.v
105105

106106
convex.v
107+
108+
hahn_banach_theorem.v
109+
107110
charge.v
108111
kernel.v
109112
pi_irrational.v

0 commit comments

Comments
 (0)