feat(Order/CompleteLatticeIntervals): ConditionallyCompleteLinearOrderBot for Set.Iio

[staroperator]

Set.Iio a (when it's nonempty) inherits the ConditionallyCompleteLinearOrderBot structure from the base type. This is commonly used in set theory, where we consider the ordinals within a, and convert Iio a from/to Ordinal.

There should also be a ConditionallyCompleteLinearOrder instance, but adding this seems difficult for now because the junk value may not be the same as bottom (which has been mentioned as "refactor that will allow different
default values for sSup and sInf" in the module doc). Since my motivation is for the ordinals purely, this PR only adds a single ConditionallyCompleteLinearOrderBot instance.

---

I'm not very familiar with the API design here, so any suggestion would be helpful.

[github-actions]

PR summary c3e588b468

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Set.Iio.coe_iInf
+ Set.Iio.coe_iSup
+ Set.Iio.coe_sInf
+ Set.Iio.coe_sSup
+ Set.Iio.conditionallyCompleteLinearOrderBot
+ coe_bot
+ coe_sup
+ instance [Lattice α] [IsLinearOrder α (· ≤ ·)] {a : α} : Lattice (Iio a)
+ isGreatest_Ioi_top
+ orderBot
+ semilatticeSup

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

[vihdzp]

There should also be a ConditionallyCompleteLinearOrder instance, but adding this seems difficult for now because the junk value may not be the same as bottom.

This is part of the reason why I've been wishing for some base typeclass for suprema/infima which states that they take on the correct values for all sets where a LUB/GLB exists. We've been floating around ideas like these for a few months, see this Zulip thread.

[vihdzp]

I feel uncomfortable making things such as sInf (∅ : Iio 5) = ∅ into theorems.

[staroperator]

I feel uncomfortable making things such as sInf (∅ : Iio 5) = ∅ into theorems.

I don't think this type checks? If you write it as sInf (∅ : Set (Iio 5)) = (⊥ : Iio 5), this looks fine to me.