[Merged by Bors] - feat(measure_theory/borel_space): a preconnected set is measurable

[ADedecker]

In a conditionally complete linear order equipped with the order topology and the corresponding borel σ-algebra, any preconnected set is measurable.

---

[sgouezel]

For all applications, I agree that conditionally_complete_linear_order is reasonable. I'm wondering if this is necessary for the statement, though: a proof assuming just linear_order would be even more satisfactory!

(Hint: consider the union u of open intervals (x, y) for x, y in s. It is open, so measurable, and contained in s. I claim that s \ u is finite, therefore measurable. In fact, it contains at most 2 points: if it contained three, one would be between the others, and therefore in u, a contradiction). For this argument, you don't even need that s is preconnected, only that it contains [x, y] whenever it contains x and y (which is implied by preconnectedness, thanks to is_preconnected.Icc_subset).

[ADedecker]

For all applications, I agree that conditionally_complete_linear_order is reasonable. I'm wondering if this is necessary for the statement, though: a proof assuming just linear_order would be even more satisfactory!

(Hint: consider the union u of open intervals (x, y) for x, y in s. It is open, so measurable, and contained in s. I claim that s \ u is finite, therefore measurable. In fact, it contains at most 2 points: if it contained three, one would be between the others, and therefore in u, a contradiction). For this argument, you don't even need that s is preconnected, only that it contains [x, y] whenever it contains x and y (which is implied by preconnectedness, thanks to is_preconnected.Icc_subset).

Indeed, that's a nice proof, I'll do it !

[bors]

✌️ ADedecker can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[sgouezel]

bors d+

[ADedecker]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests