Commit 2021-12-26 03:49 daab3ac4
View on Github →feat(data/pi/interval): Dependent functions to locally finite orders are locally finite (#11050)
This provides the locally finite order instance for Π i, α i where the α i are locally finite.
feat(data/pi/interval): Dependent functions to locally finite orders are locally finite (#11050)
This provides the locally finite order instance for Π i, α i where the α i are locally finite.