Zorn and Hahn-Banach theorems

[mkerjean]

This is in beginner's style and should heavily rewritten. It contains two files:

• hahnbanach.v contains a new formalization of Zorn's Lemma depending of the Choice in Prop and to Excluding middle, as well as a proof of Hahn_Banach theorem in its analytical form. This file is independent from MathComp Analysis libraries.

• hahnbanach_normedtype.v contains a formalization of Hahn Banach's theorem on normed vector spaces, using the Mathematical Components libraries.

[pi8027]

So this is the PR that needs linting and refactoring, right?

[mkerjean]

So this is the PR that needs linting and refactoring, right?

Yes, quite heavily. In particular, hahn_banach.v could be transformed in a file depending of mathcomp-analysis, containing another (?) proof of Zorn's lemma or using the one already present in analysis.

[affeldt-aist]

So this is the PR that needs linting and refactoring, right?

Yes, quite heavily. In particular, hahn_banach.v could be transformed in a file depending of mathcomp-analysis, containing another (?) proof of Zorn's lemma or using the one already present in analysis.

@pi8027 There a few more concrete hints in the minutes of the last meeting (https://github.com/math-comp/analysis/wiki/2021-03-26-Meeting).

[pi8027]

Could someone grant me write permission to directly push to here?

ERROR: Permission to math-comp/analysis.git denied to pi8027.

[CohenCyril]

Could someone grant me write permission to directly push to here?

ERROR: Permission to math-comp/analysis.git denied to pi8027.

done

[pi8027]

@CohenCyril Thanks!

[mkerjean]

Hi @pi8027, did you try to lint and refactor this or can I tackle this ?