mathlib3
3abee054 - chore(order/pfilter): more `principal` API (#14759)

Commit

3 years ago

chore(order/pfilter): more `principal` API (#14759) `principal` and `Inf` form a Galois coinsertion.

Author

kbuzzard

Parents