dist

Mathlib.Geometry.Metric.Abstract

Packages

Module

Theorems

750

Declarations

1016

Untrusted sidecar

Source text and display overlays are presentation metadata. The signed certificate and checker result are the trusted evidence.

Statement

forall (Scalar : Sort u), forall (sqrt_fn : forall (a : Scalar), Scalar), forall (Vector : Sort v), forall (inner : forall (x : Vector), forall (y : Vector), Scalar), forall (PointCarrier : Sort p), forall (disp_op : forall (A : PointCarrier), forall (B : PointCarrier), Vector), forall (A : PointCarrier), forall (B : PointCarrier), Scalar

Proof term

fun Scalar => fun sqrt_fn => fun Vector => fun inner => fun PointCarrier => fun disp_op => fun A => fun B => @sqrt.{u} Scalar sqrt_fn (@distSqPoints.{p,u,v} Scalar Vector inner PointCarrier disp_op A B)