generalize definitions introduced with Banach-Steinhaus PR

Open affeldt-aist opened this issue 1 year ago • 2 comments

The formalization of Baire and Banach-Steinhaus theorems (PR https://github.com/math-comp/analysis/pull/334) led to the introduction of the following definitions:

bounded_fun_norm
pointwise_bounded
uniform_bounded

See commit https://github.com/math-comp/analysis/commit/3828a154f96d3027f09f7b9237203d59fd21f25e (note that it erroneously refers to PR https://github.com/math-comp/analysis/pull/1107 that has been turned into PR https://github.com/math-comp/analysis/pull/1300)

They should actually be generalized once the PR on Topological vector spaces https://github.com/math-comp/analysis/pull/1300 is completed

@Villetaneuse

Sep 06 '24 03:09 affeldt-aist

Note that this can be addressed now that topological vector spaces have been merged.

Dec 18 '24 22:12 affeldt-aist

should we postpone this issue to the next milestone?

Feb 12 '25 07:02 affeldt-aist