mathlib

4ac13d92 - feat(data/dfinsupp/interval): Finitely supported dependent functions to locally finite orders are locally finite (#11175)

feat(data/dfinsupp/interval): Finitely supported dependent functions to locally finite orders are locally finite (#11175) This provides the ` locally_finite_order` instance for `Π₀ i, α i` in a new file `data.dfinsupp.interval`.