ContractiveOn

Mathlib.Analysis.FixedPoint.Banach

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 (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (Vector : Sort v), forall (vzero : Vector), forall (vadd : forall (x : Vector), forall (y : Vector), Vector), forall (vneg : forall (x : Vector), Vector), forall (smul : forall (a : Scalar), forall (x : Vector), Vector), forall (norm : forall (x : Vector), Scalar), forall (domain : forall (x : Vector), Prop), forall (T : forall (x : Vector), Vector), forall (k : Scalar), Prop

Proof term

fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun Vector => fun vzero => fun vadd => fun vneg => fun smul => fun norm => fun domain => fun T => fun k => forall (x : Vector), forall (y : Vector), forall (hx : domain x), forall (hy : domain y), le_rel (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm (T x) (T y)) (mul k (@NormDist.{u,v} Scalar zero one add neg sub mul le_rel Vector vzero vadd vneg smul norm x y))