import AutoSamplingTheory.TechnicalLemmas.Measure.SupportLocalBlocks

#check AutoSamplingTheory.TechnicalLemmas.Measure.SupportLocalBlocks.restrict_mass_pos_of_mem_support_of_isOpen
#check AutoSamplingTheory.TechnicalLemmas.Measure.SupportLocalBlocks.sum_restrict_le_of_pairwiseDisjoint_open
#check AutoSamplingTheory.TechnicalLemmas.Measure.SupportLocalBlocks.rectangle_restrict_mass_pos
#check AutoSamplingTheory.TechnicalLemmas.Measure.SupportLocalBlocks.exists_positive_local_blocks_of_cycleValue_pos