Def continuous_linear_map.of_is_closed_graph

Modification history

2022-06-06 20:46

src/analysis/normed_space/banach.lean

feat(analysis/normed_space/banach): closed graph theorem (#14265)

Added continuous_linear_map.of_is_closed_graph View on Github →