Commit 2023-06-05 04:51 6cb58e7b

View on Github →

feat: port Analysis.InnerProductSpace.EuclideanDist (#4675)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean

added theorem ContDiff.euclidean_dist

added def Euclidean.ball

added theorem Euclidean.ball_eq_preimage

added theorem Euclidean.ball_mem_nhds

added theorem Euclidean.ball_subset_closedBall

added def Euclidean.closedBall

added theorem Euclidean.closedBall_eq_image

added theorem Euclidean.closedBall_eq_preimage

added theorem Euclidean.closedBall_mem_nhds

added theorem Euclidean.isClosed_closedBall

added theorem Euclidean.isOpen_ball

added theorem Euclidean.mem_ball_self

added theorem Euclidean.nhds_basis_ball

added theorem Euclidean.nhds_basis_closedBall

added def toEuclidean