local_inverse_evidence_intro

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 (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (f : forall (x : X), Y), forall (point : X), forall (df : forall (h : X), Y), forall (df_inv : forall (y : Y), X), forall (op_norm : Scalar), forall (inv_op_norm : Scalar), forall (x_domain : forall (x : X), Prop), forall (y_domain : forall (y : Y), Prop), forall (inverse : forall (y : Y), X), forall (inverse_bound : Scalar), forall (inverse_remainder : forall (r : X), Prop), forall (base_mem_law : x_domain point), forall (image_mem_law : y_domain (f point)), forall (inverse_maps_law : forall (target : Y), forall (target_mem : y_domain target), x_domain (inverse target)), forall (left_inverse_law : forall (target : Y), forall (target_mem : y_domain target), @Eq.{w} Y (f (inverse target)) target), forall (right_inverse_law : forall (x : X), forall (x_mem : x_domain x), @Eq.{v} X (inverse (f x)) x), forall (unique_law : forall (x : X), forall (target : Y), forall (x_mem : x_domain x), forall (target_mem : y_domain target), forall (image_eq : @Eq.{w} Y (f x) target), @Eq.{v} X x (inverse target)), forall (fixed_point_law : forall (target : Y), forall (target_mem : y_domain target), @FixedPointResult.{u,v} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm x_domain (@InverseNewtonMap.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df df_inv op_norm inv_op_norm x_domain y_domain target) x_domain), forall (inverse_derivative_law : @FrechetDerivativeAt.{u,w,v} Scalar zero one add neg sub mul le_rel Y yzero yadd yneg ysmul ynorm X xzero xadd xneg xsmul xnorm inverse (f point) df_inv inverse_bound inverse_remainder), forall (linear_iso_law : @LinearIsoArgs.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm df df_inv op_norm inv_op_norm), @LocalInverseEvidence.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df df_inv op_norm inv_op_norm x_domain y_domain inverse inverse_bound inverse_remainder

fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun f => fun point => fun df => fun df_inv => fun op_norm => fun inv_op_norm => fun x_domain => fun y_domain => fun inverse => fun inverse_bound => fun inverse_remainder => fun base_mem_law => fun image_mem_law => fun inverse_maps_law => fun left_inverse_law => fun right_inverse_law => fun unique_law => fun fixed_point_law => fun inverse_derivative_law => fun linear_iso_law => fun (P : Prop) => fun (mk : forall (base_mem_law : x_domain point), forall (image_mem_law : y_domain (f point)), forall (inverse_maps_law : forall (target : Y), forall (target_mem : y_domain target), x_domain (inverse target)), forall (left_inverse_law : forall (target : Y), forall (target_mem : y_domain target), @Eq.{w} Y (f (inverse target)) target), forall (right_inverse_law : forall (x : X), forall (x_mem : x_domain x), @Eq.{v} X (inverse (f x)) x), forall (unique_law : forall (x : X), forall (target : Y), forall (x_mem : x_domain x), forall (target_mem : y_domain target), forall (image_eq : @Eq.{w} Y (f x) target), @Eq.{v} X x (inverse target)), forall (fixed_point_law : forall (target : Y), forall (target_mem : y_domain target), @FixedPointResult.{u,v} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm x_domain (@InverseNewtonMap.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df df_inv op_norm inv_op_norm x_domain y_domain target) x_domain), forall (inverse_derivative_law : @FrechetDerivativeAt.{u,w,v} Scalar zero one add neg sub mul le_rel Y yzero yadd yneg ysmul ynorm X xzero xadd xneg xsmul xnorm inverse (f point) df_inv inverse_bound inverse_remainder), forall (linear_iso_law : @LinearIsoArgs.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm df df_inv op_norm inv_op_norm), P) => mk base_mem_law image_mem_law inverse_maps_law left_inverse_law right_inverse_law unique_law fixed_point_law inverse_derivative_law linear_iso_law