OAI/Geometry/RCD/Heat/NearEndpointTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Transfer of a normalized endpoint estimate to nearby points

  1. theorem OAI.RegularPointCoordinates.near_endpoint_transfer line 12