Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous_linear_map.coe_of_seq_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.coe_of_seq_closed_graphView on Github →