This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
[Merged by Bors] - feat(measure_theory/order/upper_lower): Order-connected sets in ℝⁿ are measurable
#7365
YaelDilliesadd_ported_warnings.yml
on: pull_request
Check for modifications to ported files
29s
Annotations
5 warnings
|
Check for modifications to ported files:
src/analysis/normed/order/upper_lower.lean#L1
Changes to this file will need to be ported to mathlib 4!
Please consider retracting the changes to this file unless you are willing to immediately forward-port them.
|
|
Check for modifications to ported files:
src/data/real/nnreal.lean#L1
Changes to this file will need to be ported to mathlib 4!
Please consider retracting the changes to this file unless you are willing to immediately forward-port them.
|
|
Check for modifications to ported files:
src/order/bounds/basic.lean#L1
Changes to this file will need to be ported to mathlib 4!
Please consider retracting the changes to this file unless you are willing to immediately forward-port them.
|
|
Check for modifications to ported files:
src/topology/algebra/order/upper_lower.lean#L1
Changes to this file will need to be ported to mathlib 4!
Please consider retracting the changes to this file unless you are willing to immediately forward-port them.
|
|
Check for modifications to ported files
The process '/usr/bin/git' failed with exit code 128
|