[Merged by Bors] - feat: sup-closed sets are closed under finite suprema

[YaelDillies]

From GrowthInGroups

---

[github-actions]

PR summary 2b14177317

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Order.SupClosed	512	515	+3 (+0.59%)

Import changes for all files

Files	Import difference
5 files Mathlib.Combinatorics.SetFamily.FourFunctions Mathlib.Combinatorics.SetFamily.Compression.UV Mathlib.Combinatorics.SetFamily.Shadow Mathlib.Combinatorics.SetFamily.LYM Mathlib.Combinatorics.SetFamily.KruskalKatona	1
3 files Mathlib.Algebra.Module.Submodule.Invariant Mathlib.Combinatorics.SetFamily.AhlswedeZhang Mathlib.Combinatorics.Colex	2
5 files Mathlib.Order.CompleteSublattice Mathlib.Data.Finset.Sups Mathlib.Data.Set.Sups Mathlib.Order.SupClosed Mathlib.Order.Sublattice	3

---

Declarations diff

+ InfClosed.biInf_mem
+ InfClosed.biInf_mem_of_nonempty
+ InfClosed.iInf_mem
+ InfClosed.iInf_mem_of_nonempty
+ InfClosed.sInf_mem
+ InfClosed.sInf_mem_of_nonempty
+ SupClosed.biSup_mem
+ SupClosed.biSup_mem_of_nonempty
+ SupClosed.iSup_mem
+ SupClosed.iSup_mem_of_nonempty
+ SupClosed.sSup_mem
+ SupClosed.sSup_mem_of_nonempty

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.

[b-mehta]

Suggested change

	lemma SupClosed.iSup_mem_of_nonempty [Finite ι] [Nonempty ι] (hs : SupClosed s)
	lemma SupClosed.ciSup_mem [Finite ι] [Nonempty ι] (hs : SupClosed s)

[YaelDillies]

I disagree with this name. This lemma is also valid (and useful) for complete lattices, and the current name helps disambiguate from the other iSup_mem lemma.

[b-mehta]

Suggested change

	lemma InfClosed.iInf_mem_of_nonempty [Finite ι] [Nonempty ι] (hs : InfClosed s)
	lemma InfClosed.ciInf_mem [Finite ι] [Nonempty ι] (hs : InfClosed s)

[b-mehta]

Suggested change

	lemma SupClosed.sSup_mem_of_nonempty (hs : SupClosed s) (ht : t.Finite) (ht' : t.Nonempty)
	lemma SupClosed.csSup_mem (hs : SupClosed s) (ht : t.Finite) (ht' : t.Nonempty)

[b-mehta]

Suggested change

	lemma InfClosed.sInf_mem_of_nonempty (hs : InfClosed s) (ht : t.Finite) (ht' : t.Nonempty)
	lemma InfClosed.csInf_mem (hs : InfClosed s) (ht : t.Finite) (ht' : t.Nonempty)

[b-mehta]

I'm not convinced of the names still, but since they're in a namespace I guess it's not so bad that these are inconsistent

bors d+

[mathlib-bors]

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[YaelDillies]

*consistent in a way you don't see 😉

bors merge

[b-mehta]

*consistent in a way you don't see 😉

Note that there are exactly zero other lemmas in mathlib that take a supremum over a general conditionally complete lattice and have the name iSup. And there are many other lemmas in mathlib that take a supremum over a general conditionally complete lattice that also work for complete lattices, and are still called ciSup. And, as pointed out on the zulip thread, the disambiguation argument doesn't hold if there are more lemmas in mathlib.
So I would like to see some more factual arguments that this is consistent, as currently this is objectively increasing inconsistency in mathlib 😉

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style

[YaelDillies]

Note that there are exactly zero other lemmas in mathlib that take a supremum over a general conditionally complete lattice and have the name iSup.

There are at least three or four according to https://loogle.lean-lang.org/?q=iSup%2C+ConditionallyCompleteLattice