Commit 2026-10-30 20:28 a36db84c

refactor(MeasureTheory/Constructions/BorelSpace/Order): regroup sections and weaken hypotheses (#45475) Regroup the sections of BorelSpace/Order.lean so that repeated instance binders become section variables, and weaken BorelSpace to OpensMeasurableSpace where the proofs allow it:

• the lt/le lemmas and Measurable.max/min now share a section with [SecondCountableTopology α] [OrderClosedTopology α] instead of repeating these binders;
• MeasurableSet.of_mem_nhdsGT_aux and MeasurableSet.of_mem_nhdsGT move next to them under [OrderTopology α], and only assume [OpensMeasurableSpace α] (their proofs only use measurability of open sets, singletons and countable sets);
• Monotone.measurable, Antitone.measurable, aemeasurable_restrict_of_monotoneOn and aemeasurable_restrict_of_antitoneOn only assume [OpensMeasurableSpace β] on the domain, matching Continuous.measurable. The section-wide [BorelSpace β] they inherited is kept only for measurable_iSup_of_lowerSemicontinuous/iInf_of_upperSemicontinuous, where β is the codomain. No proofs change except the two Antitone lemmas, whose positional @ applications are rewritten with named arguments. Preparation for #42164.