Mathlib Changelog
Changelog
About
Github
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