interval): Dependent functions to locally finite orders are locally finite (#11050)

Commit

3 years ago

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.

Author

YaelDillies

Parents

2e2510ee

mathlib daab3ac4 - feat(data/pi/interval): Dependent functions to locally finite orders are locally finite (#11050)

mathlib
daab3ac4 - feat(data/pi/interval): Dependent functions to locally finite orders are locally finite (#11050)