`vsub` (#4751)

Commit

5 years ago

feat(analysis/normed_space/add_torsor): continuity of `vadd`/`vsub` (#4751) Prove that `vadd`/`vsub` are Lipschitz continuous, hence uniform continuous and continuous.

References

#4925 - Make prime-avoidance branch build

Author

urkud

Parents

e7a4b12c

mathlib a9d3ce8e - feat(analysis/normed_space/add_torsor): continuity of `vadd`/`vsub` (#4751)

mathlib
a9d3ce8e - feat(analysis/normed_space/add_torsor): continuity of `vadd`/`vsub` (#4751)