Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-06 20:46 d28aa2c9

View on Github →

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

Estimated changes

Modified src/analysis/normed_space/banach.lean

added theorem continuous_linear_map.coe_fn_of_is_closed_graph

added theorem continuous_linear_map.coe_fn_of_seq_closed_graph

added theorem continuous_linear_map.coe_of_is_closed_graph

added theorem continuous_linear_map.coe_of_seq_closed_graph

added def continuous_linear_map.of_is_closed_graph

added def continuous_linear_map.of_seq_closed_graph

added theorem linear_map.continuous_of_is_closed_graph

added theorem linear_map.continuous_of_seq_closed_graph