# Commit 2022-01-11 13:55 4ac13d92

View on Github →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`

.