Mathlib v3 is deprecated. Go to Mathlib v4

Theorem linear_map.continuous_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 linear_map.continuous_of_is_closed_graphView on Github →