Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2020-08-05 09:56
37119b41
View on Github →
feat(topology): normed spaces are (locally) path connected (
#3689
)
Estimated changes
Modified
src/analysis/convex/topology.lean
added
theorem
convex.is_path_connected
Modified
src/topology/algebra/module.lean
Modified
src/topology/continuous_on.lean
added
theorem
continuous_on.comp_continuous
Modified
src/topology/metric_space/basic.lean
added
theorem
metric.nonempty_ball
added
theorem
metric.nonempty_closed_ball
Modified
src/topology/path_connected.lean
added
theorem
joined_in.of_line
added
def
path.of_line
added
theorem
path.of_line_mem