Recent Commits to mathlib:master

Stream: general

[Ruben Van de Velde]

rss-bot said:

feat(measure_theory/order/upper_lower): Order-connected sets in ℝⁿ are measurable (mathlib#16976)

Prove that the frontier of an order-connected set in ℝⁿ (with the ∞-metric, but it doesn't actually matter) has measure zero.

As a corollary, antichains in ℝⁿ have measure zero.

Co-authored-by: @JasonKYi

Authored-by: YaelDillies (commit)

Why does this add a mathport submodule? @Yaël Dillies

[Yaël Dillies]

Uh, that's an accident.

[Yaël Dillies]

This is really annoying because it doesn't show as a modification in the vscode interface.

[Eric Wieser]

I think we should probably force-push a correction to that commit

[Eric Wieser]

I can see submodule breaking tooling in unexpected ways there

[Eric Wieser]

(done)