Theorems · Definition · functional analysis

Euclidean.dist

{E : Type u_1} →
  [inst : AddCommGroup E] →
    [inst_1 : TopologicalSpace E] →
      [IsTopologicalAddGroup E] →
        [T2Space E] → [inst_4 : Module ℝ E] → [ContinuousSMul ℝ E] → [FiniteDimensional ℝ E] → E → E → ℝ

If x and y are two points in a finite-dimensional space over ℝ, then Euclidean.dist x y is the distance between these points in the metric defined by some inner product space structure on E.

Defined in

Mathlib.Analysis.InnerProductSpace.EuclideanDist

Cited by

2 results in Mathlib

Foundations

Depth 226 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupTopologicalSpaceIsTopologicalAddGroupT2SpaceModuleContinuousSMulFiniteDimensional