test module
Tests.PairingCycleQuantitativeNeighborhood
0 named declarations scanned from Tests/PairingCycleQuantitativeNeighborhood.lean.
Declarations
This aggregator contains no named declarations.
Complete Lean source
Tests/PairingCycleQuantitativeNeighborhood.lean — full module with imports and context
import AutoSamplingTheory.TechnicalLemmas.Analysis.PairingCycleQuantitativeNeighborhood
#check AutoSamplingTheory.TechnicalLemmas.Analysis.PairingCycleQuantitativeNeighborhood.exists_pairwiseDisjoint_bounded_open_rectangles_of_cycleValue_pos