[Merged by Bors] - feat: Topological properties of order-connected sets in ℝⁿ

[YaelDillies]

Partially forward-port leanprover-community/mathlib3#16976

---

• depends on: [Merged by Bors] - feat: Real.toNNReal_abs #11606

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: Real.toNNReal_abs #11606
  By Dependent Issues (🤖). Happy coding!

[Ruben-VandeVelde]

Seems pretty straightforward, modulo the removal of Topology.Order.Bounded

[github-actions]

Import summary

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Normed.Order.UpperLower	1150	1153	+3 (+0.26%)

[Ruben-VandeVelde]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

[fpvandoorn]

One more comment. Feel free to merge even if you disagree.

bors d+

[mathlib-bors]

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

[j-loreaux]

This comment shouldn't hold up this PR, but the relevant lemmas could just take a homeomorphism with a pi-type as an explicit argument. It's not a pretty solution, but I think it would work, and I believe we already have the necessary homeomorphisms available.

(On second thought, would it need to be an order isomorphism too? That probably rules out this idea as being useful)

[YaelDillies]

Yeah, it would also need to be an order isomorphism. That's the crux. We need a way to say "Order on this type is given by those coordinates", which sounds a lot like the Inducing/Embedding business in the topology part of the library.

Food for thought, I guess

[YaelDillies]

bors merge

[github-actions]

PR summary

Import changes

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Normed.Order.UpperLower	1150	1153	+3 (+0.26%)

---

Diff of declarations

+ BddAbove.isBounded
+ BddAbove.isBounded_inter
+ BddBelow.isBounded
+ BddBelow.isBounded_inter
+ Bornology.IsBounded.bddAbove
+ Bornology.IsBounded.bddBelow
+ Bornology.IsBounded.subset_Icc_sInf_sSup
+ IsClopen.lowerClosure_pi
+ IsClopen.upperClosure_pi
+ IsClosed.lowerClosure_pi
+ IsClosed.upperClosure_pi
+ IsOrderBornology
+ OrderDual.instIsOrderBornology
+ Pi.instIsOrderBornology
+ Prod.instIsOrderBornology
+ _root_.BddAbove.isBoundedUnder
+ _root_.BddBelow.isBoundedUnder
+ bddAbove_preimage_ofDual
+ bddAbove_preimage_toDual
+ bddBelow_preimage_ofDual
+ bddBelow_preimage_toDual
+ closure_lowerClosure_comm_pi
+ closure_upperClosure_comm_pi
+ dist_anti_left_pi
+ dist_anti_right_pi
+ dist_inf_sup_pi
+ dist_le_dist_of_le_pi
+ dist_mono_left_pi
+ dist_mono_right_pi
+ instBornology
+ instIsOrderBornology
+ isBounded_iff_bddBelow_bddAbove
+ isBounded_preimage_ofDual
+ isBounded_preimage_toDual
+ isCobounded_preimage_ofDual
+ isCobounded_preimage_toDual
+ isOrderBornology_iff_eq_orderBornology
+ lowerClosure_interior_subset'
+ orderBornology
+ orderBornology_isBounded
+ upperClosure_interior_subset'
- Real.isBounded_iff_bddBelow_bddAbove
- Real.subset_Icc_sInf_sSup_of_isBounded

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[mathlib-bors]

Canceled.

[YaelDillies]

bors merge

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style