feat(Order/Partition): finite meets of partitions of frames

[peabrainiac]

For any frame α, Partition α has finite meets: the meet of two partitions P, Q can be constructed as the partition consisting of all meets p ⊓ q with p ∈ P, q ∈ Q and p ⊓ q ≠ ⊥.

Note that even for frames Partition α does not have arbitrary meets: for example, there is no finest partition on the frame of open subsets of the Cantor space. We thus have to construct the remaining operations by hand instead of e.g. just transporting a CompleteLattice instance along some Galois connection.

---

[github-actions]

PR summary 34f85c5f24

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ instance {α : Type*} [Order.Frame α] {s : α} : SemilatticeInf (Partition s)
+ mem_inf_iff

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).