New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(measure_theory/order/upper_lower): Order-connected sets in ℝⁿ
are measurable
#16976
Conversation
upper sets form a monoid upper set of open is open antichains have measure zero
de2d60b
to
74370c4
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
ℝⁿ
are measurableℝⁿ
are measurable
* Add `upperBounds_closure`, `lowerBounds_closure`, `bddAbove_closure`, `bddBelow_closure`. * Add `IsAntichain.interior_eq_empty`. * Generalize `nhds_left'_le_nhds_ne` and `nhds_right'_le_nhds_ne` to a `Preorder`. Partly forward-ports leanprover-community/mathlib#16976
* Add `upperBounds_closure`, `lowerBounds_closure`, `bddAbove_closure`, `bddBelow_closure`. * Add `IsAntichain.interior_eq_empty`. * Generalize `nhds_left'_le_nhds_ne` and `nhds_right'_le_nhds_ne` to a `Preorder`. Partly forward-ports leanprover-community/mathlib#16976
* Add `upperBounds_closure`, `lowerBounds_closure`, `bddAbove_closure`, `bddBelow_closure`. * Add `IsAntichain.interior_eq_empty`. * Generalize `nhds_left'_le_nhds_ne` and `nhds_right'_le_nhds_ne` to a `Preorder`. Partly forward-ports leanprover-community/mathlib#16976
Partially forward-port leanprover-community/mathlib#16976
Partially forward-port leanprover-community/mathlib#16976 Also fix an unused argument that somehow made it to master, likely from #10661.
Partially forward-port leanprover-community/mathlib#16976 Also fix an unused argument that somehow made it to master, likely from #10661.
Partially forward-port leanprover-community/mathlib#16976 Also fix an unused argument that somehow made it to master, likely from #10661.
Partially forward-port leanprover-community/mathlib#16976 Also fix an unused argument that somehow made it to master, likely from #10661.
Partially forward-port leanprover-community/mathlib#16976 Also fix an unused argument that somehow made it to master, likely from #10661.
Partially forward-port leanprover-community/mathlib#16976 Also fix an unused argument that somehow made it to master, likely from #10661.
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
ennreal.of_real
#16955nhds_within
versions #16956a * b ≠ b ↔ a ≠ 1
#18635This is a three lines remark in Reverse Kleitman Inequalities, Bollobas, Leader, Radcliffe, with no proof. So Jason, Bhavik and I came up with a proof using Lebesgue Density Theorem.