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
.