Skip to content

continuous_linear_bounded should be generalized to convexTvsType #1927

@affeldt-aist

Description

@affeldt-aist

Lemma continuous_linear_bounded (x : V) (f : {linear V -> W}) :

but this will cause generalization of other intermediate lemmas such as bounded_near

this will be necessary to generalize the forthcoming Hahn-Banach theorem

@mkerjean

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancement ✨This issue/PR is about adding new features enhancing the library

    Type

    No type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions