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.
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.