Partition refinement
= Partition refinement
A refinement of a finite interval partition inserts additional points without removing original points. The union of two partitions is a common refinement. Refinement makes each subinterval smaller, increasing its infimum and decreasing its supremum; this proves <Darboux sum refinement monotonicity>.