interval): The lexicographic sum of two locally finite orders is locally finite (#11352)

Commit

2 years ago

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

Author

YaelDillies

Parents

3ba15165

mathlib 48a058d7 - feat(data/sum/interval): The lexicographic sum of two locally finite orders is locally finite (#11352)

mathlib
48a058d7 - feat(data/sum/interval): The lexicographic sum of two locally finite orders is locally finite (#11352)