Commit 2026-09-15 14:11 78f7ceb7

View on Github →

chore: rename (anti)lipschitz to (anti)lipschitzWith (#43724) This PR renames

  • SemilinearIsometryClass.lipschitz -> SemilinearIsometryClass.lipschitzWith
  • SemilinearIsometryClass.antilipschitz -> SemilinearIsometryClass.antilipschitzWith
  • LinearIsometry.lipschitz -> LinearIsometry.lipschitzWith
  • LinearIsometry.antilipschitz -> LinearIsometry.antilipschitzWith
  • LinearIsometryEquiv.lipschitz -> LinearIsometryEquiv.lipschitzWith
  • Dilation.lipschitz -> Dilation.lipschitzWith
  • Dilation.antilipschitz -> Dilation.antilipschitzWith

Estimated changes

deleted theorem Dilation.antilipschitz
deleted theorem Dilation.lipschitz
added theorem Dilation.lipschitzWith