[Merged by Bors] - feat: basic API for ConditionallyCompletePartialOrder

[j-loreaux]

This develops the basic API for ConditionallyCompletePartialOrder. The API is copied from ConditionallyCompleteLattice, with DirectedOn assumptions added, and these lemmas are protected within that namespace. In a few cases, the lemmas were capable of being generalized outright, which we have done here.

As a result, some material moved out of ConditionallyCompleteLattice/Basic to ConditionallyCompletePartialOrder/Basic.

---

• depends on: [Merged by Bors] - feat: define ConditionallyCompletePartialOrder #35046

[github-actions]

PR summary ca1d0aeba0

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Order.ConditionallyCompleteLattice.Indexed	245	248	+3 (+1.22%)

Import changes for all files

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

---

Declarations diff

+ Directed.Ici_ciSup
+ Directed.ciInf_le_ciSup
+ Directed.ciSup_eq_of_forall_le_of_forall_lt_exists_gt
+ Directed.ciSup_le_iff
+ Directed.ciSup_mono
+ Directed.isLUB_ciSup
+ Directed.le_ciSup_of_le
+ DirectedOn.ciSup_set_le_iff
+ DirectedOn.csInf_le_csSup
+ DirectedOn.csSup_eq_of_forall_le_of_forall_lt_exists_gt
+ DirectedOn.csSup_le_csSup
+ DirectedOn.csSup_le_iff
+ DirectedOn.isDirectedOrder
+ DirectedOn.isLUB_ciSup_set
+ DirectedOn.le_ciSup_set
+ DirectedOn.le_csSup_iff
+ DirectedOn.le_csSup_of_le
+ DirectedOn.lt_csSup_of_lt
+ DirectedOn.notMem_of_csSup_lt
+ DirectedOn.of_isDirectedOrder
+ DirectedOn.subset_Icc_csInf_csSup
+ IsGreatest.directedOn
+ directedOn_iff_isDirectedOrder
+ instance (priority := 100) CompleteLattice.toCompletePartialOrder [CompleteLattice α] :
+ instance (priority := 100) CompletePartialOrder.toOmegaCompletePartialOrder :
+ instance (priority := 100) ConditionallyCompleteLattice.toConditionallyCompletePartialOrder :
+ instance (priority := 100) [CompletePartialOrder α] : ConditionallyCompletePartialOrderSup α
+ instance [ConditionallyCompletePartialOrder α] :
+ instance [ConditionallyCompletePartialOrderInf α] :
+ instance [ConditionallyCompletePartialOrderSup α] :
+ l_ciSup_of_directed
+ l_ciSup_set_of_directedOn
+ l_csSup_of_directedOn
+ l_csSup_of_directedOn'
+ map_ciInf_of_directed
+ map_ciInf_set_of_directedOn
+ map_ciSup_of_directed
+ map_ciSup_set_of_directedOn
+ map_csInf_of_directedOn
+ map_csInf_of_directedOn'
+ map_csSup_of_directedOn
+ map_csSup_of_directedOn'
+ u_ciInf_of_directed
+ u_ciInf_set_of_directedOn
+ u_csInf_of_directedOn
+ u_csInf_of_directedOn'
- CompleteLattice.toCompletePartialOrder
- CompletePartialOrder.toOmegaCompletePartialOrder
- IsLeast.csInf_eq
- IsLeast.csInf_mem
- cbiInf_eq_of_forall
- ciInf_Ici
- ciInf_const
- ciInf_eq_ite
- ciInf_neg
- ciInf_pos
- ciInf_subsingleton
- ciInf_unique
- csInf_singleton
- iInf_congr_Prop
- iInf_of_isEmpty
- inf_eq_bot_of_bot_mem
- sInf_image'

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

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat: define ConditionallyCompletePartialOrder #35046
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[j-loreaux]

@b-mehta for review, it may be easiest to do in two batches of commits: everything prior to but not including eda5b56, and then everything after and including that commit. The stuff that comes before is just sSup-related, and the stuff after is iSup-related. If you want , I can split these into two PRs, but I thought it made sense to do it all at once.

[b-mehta]

This looks good to me! Thanks for this!

The one thing I'm unsure about is if the WithTop/SupSet (and dual) stuff should be in this file or elsewhere - it's not really specific to CCPOs. What do you think about putting that in a separate file?

bors d+

[mathlib-bors]

✌️ j-loreaux 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]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Lint style
• ci (staging) / Post-CI job
• ci (staging) / Post-Build Step
• ci (staging) / Build

[kbuzzard]

!radar

[leanprover-radar]

Benchmark results for 086cbab against ca1d0ae are in! @kbuzzard

• 🟥 build//instructions: +316.9G (+0.17%)

Medium changes (4🟥)

• 🟥 build/module/Mathlib.Order.CompleteLatticeIntervals//instructions: +4.0G (+25.12%)
• 🟥 build/module/Mathlib.Order.CompleteSublattice//instructions: +1.6G (+12.90%)
• 🟥 build/module/Mathlib.Probability.Process.Filtration//instructions: +7.7G (+31.63%)
• 🟥 build/module/Mathlib.Topology.Sets.Closeds//instructions: +2.9G (+15.15%)

Small changes (2✅, 29🟥)

Too many entries to display here. View the full report on radar instead.