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.

Estimated changes