OAI/Geometry/RCD/Transport/CompactCouplingSlack.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compact limits of couplings with vanishing dual slack

  1. theorem OAI.RegularPointCoordinates.coupling_snd_support line 19
  2. theorem OAI.RegularPointCoordinates.compact_coupling_zero_slack line 25