noncomputable def Euclidean.norm {n : ℕ} (a : Fin n → ℝ) : ℝ

Equations

• Euclidean.norm a = √(∑ i : Fin n, a i ^ 2)

noncomputable def Euclidean.dist {n : ℕ} (a b : Fin n → ℝ) : ℝ

Equations

• Euclidean.dist a b = Euclidean.norm (a - b)

theorem Euclidean.dist_triangle_aux₁ {a b x y : ℝ} : a * b + x * y ≤ b ^ 2 + √((x ^ 2 + b ^ 2) * (y ^ 2 + (a - b) ^ 2))

theorem Euclidean.dist_triangle {n : ℕ} {a b c : Fin n → ℝ} : Euclidean.dist a c ≤ Euclidean.dist a b + Euclidean.dist b c

@[instance_reducible]

noncomputable def Euclidean.instNormForallFinReal_projects {n : ℕ} : Norm (Fin n → ℝ)

Equations

• Euclidean.instNormForallFinReal_projects = { norm := Euclidean.norm }

@[instance_reducible]

noncomputable def Euclidean.instDistForallFinReal_projects {n : ℕ} : Dist (Fin n → ℝ)

Equations

• Euclidean.instDistForallFinReal_projects = { dist := Euclidean.dist }

theorem Euclidean.norm_def {n : ℕ} {a : Fin n → ℝ} : ‖a‖ = Euclidean.norm a

theorem Euclidean.dist_def {n : ℕ} {a b : Fin n → ℝ} : dist a b = Euclidean.dist a b

@[instance_reducible]

noncomputable def Euclidean.instPseudoMetricSpaceForallFinReal_projects {n : ℕ} : PseudoMetricSpace (Fin n → ℝ)

Equations

• Euclidean.instPseudoMetricSpaceForallFinReal_projects = { toDist := Euclidean.instDistForallFinReal_projects, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist := fun (x y : Fin n → ℝ) => ↑(NNReal.mk (dist x y) ⋯), edist_dist := ⋯, toUniformSpace := UniformSpace.ofDist dist ⋯ ⋯ ⋯, uniformity_dist := ⋯, toBornology := Bornology.ofDist dist ⋯ ⋯, cobounded_sets := ⋯ }

@[instance_reducible]

noncomputable def Euclidean.instMetricSpaceForallFinReal_projects {n : ℕ} : MetricSpace (Fin n → ℝ)

Equations

• Euclidean.instMetricSpaceForallFinReal_projects = { toPseudoMetricSpace := Euclidean.instPseudoMetricSpaceForallFinReal_projects, eq_of_dist_eq_zero := ⋯ }