mathlib3

aece00a2 - feat(data/sigma/interval): A disjoint sum of locally finite orders is locally finite (#10929)

feat(data/sigma/interval): A disjoint sum of locally finite orders is locally finite (#10929) This provides `locally_finite_order (Σ i, α i)` in a new file `data.sigma.interval`. This also makes `<` a primitive on `Σ i, α i`.