interval): The disjoint sum of two locally finite orders is locally finite (#11351)

Commit

4 years ago

feat(data/sum/interval): The disjoint sum of two locally finite orders is locally finite (#11351) This proves `locally_finite_order (α ⊕ β)` where `α` and `β` are locally finite themselves.

Author

YaelDillies

Parents

dbf59ba1

mathlib c72e709e - feat(data/sum/interval): The disjoint sum of two locally finite orders is locally finite (#11351)

mathlib
c72e709e - feat(data/sum/interval): The disjoint sum of two locally finite orders is locally finite (#11351)