order): bounding finite fibration cardinalities from below (#4396)

Commit

5 years ago

feat(algebra/big_operators/order): bounding finite fibration cardinalities from below (#4396) Also including unrelated change `finset.inter_eq_sdiff_sdiff`.

References

#4925 - Make prime-avoidance branch build

Author

Oliver Nash

Parents

f437365a

mathlib3 d13d21ba - feat(algebra/big_operators/order): bounding finite fibration cardinalities from below (#4396)

mathlib3
d13d21ba - feat(algebra/big_operators/order): bounding finite fibration cardinalities from below (#4396)