separation): Eidelheit's theorem (#14460)

Commit

3 years ago

feat(analysis/normed_space/hahn-banach/separation): Eidelheit's theorem (#14460) Prove Eidelheit's theorem as a corollary to the geometric Hahn-Banach.

Author

YaelDillies

Parents

b6395b3a

mathlib d9e72ffb - feat(analysis/normed_space/hahn-banach/separation): Eidelheit's theorem (#14460)

mathlib
d9e72ffb - feat(analysis/normed_space/hahn-banach/separation): Eidelheit's theorem (#14460)