Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-05-10 05:02
ebf0b750
View on Github →
feat: port Analysis.Normed.Group.ControlledClosure (
#3880
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Analysis/Normed/Group/ControlledClosure.lean
added
theorem
controlled_closure_of_complete
added
theorem
controlled_closure_range_of_complete