feat(Order/OmegaCompletePartialOrder): OmegaCompletePartialOrder instance for Sigma with basic ωScottContinuous lemmas

[YellPika]

• depends on: feat(Order/OmegaCompletePartialOrder): OmegaCompletePartialOrder instance for Sum with basic ωScottContinuous lemmas #33985
• depends on: feat(Order/OmegaCompletePartialOrder): teach fun_prop about ωScottContinuous functions #33941

---

[github-actions]

PR summary 95093e961c

Import changes exceeding 2%

%	File
+5.29%	Mathlib.Order.ScottContinuity

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Order.ScottContinuity	208	219	+11 (+5.29%)
Mathlib.Order.OmegaCompletePartialOrder	350	357	+7 (+2.00%)

Import changes for all files

Files	Import difference
There are 3540 files with changed transitive imports taking up over 161647 characters: this is too many to display!
You can run scripts/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

+ ScottContinuousOn.inl
+ ScottContinuousOn.inr
+ const
+ const_coe
+ distrib
+ distrib_cases
+ distrib_inj
+ fst_mono
+ inj
+ inj_coe
+ inl
+ inl_coe
+ inr
+ inr_coe
+ instance : OmegaCompletePartialOrder ((i : ι) × ρ i)
+ instance : OmegaCompletePartialOrder (α ⊕ β)
+ mk_mono
+ ofFun
+ projl
+ projl_coe
+ projr
+ projr_coe
+ snd_mono
+ split
+ split_cases
+ split_inl
+ split_inr
+ swap_mono
+ ωScottContinuous.apply
+ ωScottContinuous.comp'
+ ωScottContinuous.const'
+ ωScottContinuous.id'
+ ωScottContinuous_apply
+ ωScottContinuous_inl
+ ωScottContinuous_inl'
+ ωScottContinuous_inr
+ ωScottContinuous_inr'
+ ωScottContinuous_map
+ ωScottContinuous_mk
+ ωSup_const
+ ωSup_inj
+ ωSup_inl
+ ωSup_inr
++ elim_mono
++ ωScottContinuous_elim
++ ωScottContinuous_fst
++ ωScottContinuous_snd

You can run this locally as follows

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

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

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(Order/OmegaCompletePartialOrder): OmegaCompletePartialOrder instance for Sum with basic ωScottContinuous lemmas #33985
• feat(Order/OmegaCompletePartialOrder): teach fun_prop about ωScottContinuous functions #33941
  By Dependent Issues (🤖). Happy coding!