# Commit 2023-08-02 16:47 48a058d7

View on Github →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.

Mathlib v3 is deprecated. Go to Mathlib v4

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.