chore: rename field inf to min in Lattice

[JovanGerb]

As suggested by @eric-wieser, this PR renames the sup and inf fields in Lattice to max and min. This means that we now can extend Lattice and LinearOrder simultaneously without ending up with duplicate fields. This should be implemented in a future PR for existing classes like CompleteLinearOrder.

Zulip discussion

---

[github-actions]

PR summary dde1cfffb6

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

- SemilatticeInf.toMin
- SemilatticeSup.toMax

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

[eric-wieser]

This avoids having duplicate fields max and sup in CompleteLinearOrder.

There is no duplication of these fields in master; I think more accurately this makes it possible to use extends without creating such duplicates. Do you intend to use extends in this PR?

[JovanGerb]

Yes, using extends seems like a good idea. I'm not sure if that should be in this PR though.

[leanprover-community-mathlib4-bot]

!bench

[leanprover-bot]

Here are the benchmark results for commit 402572c.
There were no significant changes against commit 4fefe1c.

[github-actions]

File	Instructions	%
build	-78.101⬝10⁹	(-0.04%)
lint	-16.106⬝10⁹	(-0.22%)

2 files, Instructions +3.0⬝10⁹

File	Instructions	%
Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts	+3.239⬝10⁹	(+3.29%)
Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections	+3.59⬝10⁹	(+3.86%)

File	Instructions	%
Mathlib.Algebra.Homology.HomotopyCategory.Triangulated	+1.256⬝10⁹	(+0.99%)

9 files, Instructions -2.0⬝10⁹

File	Instructions	%
Mathlib.Order.Copy	-1.116⬝10⁹	(-8.23%)
Mathlib.Algebra.Lie.Nilpotent	-1.251⬝10⁹	(-1.27%)
Mathlib.Order.CompleteBooleanAlgebra	-1.377⬝10⁹	(-3.42%)
Mathlib.Algebra.Order.Ring.Idempotent	-1.377⬝10⁹	(-7.45%)
Mathlib.Algebra.Lie.Solvable	-1.490⬝10⁹	(-3.65%)
Mathlib.AlgebraicGeometry.RationalMap	-1.508⬝10⁹	(-2.06%)
Mathlib.Order.Interval.Set.Fin	-1.613⬝10⁹	(-3.42%)
Mathlib.Order.BooleanAlgebra	-1.711⬝10⁹	(-4.95%)
Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral	-1.730⬝10⁹	(-5.52%)

2 files, Instructions -3.0⬝10⁹

File	Instructions	%
Mathlib.Analysis.Calculus.LocalExtr.Basic	-2.448⬝10⁹	(-6.81%)
Mathlib.Probability.Kernel.Proper	-2.507⬝10⁹	(-4.05%)

3 files, Instructions -4.0⬝10⁹

File	Instructions	%
Mathlib.Topology.Path	-3.405⬝10⁹	(-9.10%)
Mathlib.Data.Finset.Max	-3.465⬝10⁹	(-9.25%)
Mathlib.Order.Interval.Finset.Fin	-3.620⬝10⁹	(-6.32%)

CI run

[eric-wieser]

I'm not sure if that should be in this PR though.

Please make it clear in the description what you decided, rather that the current version which is ambiguous!

[bryangingechen]

Since these names differ from the ones used conventionally, could you please add explanation(s) to the relevant docstring(s)?

[JovanGerb]

Where do you think the doc-strings should go? On Lattice? Or SemilatticeSup/Inf? I'm reusing the max and min from the Max and Min type classes, since that is the one that's already used by the ⊔ / ⊓ notation (so I can't extend that doc-string).

[bryangingechen]

Certainly on SemilatticeSup / Inf since those definitions are where the terminology begins to differ. I'm not sure about Lattice and other structures "above" them, I guess it's a tradeoff between having the same explanation in lots of different places vs discoverability.

[leanprover-community-bot-assistant]

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

[leanprover-community-bot-assistant]

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

[eric-wieser]

I think you should ping the Zulip thread about this change, or maybe even make a new thread if the title isn't visible enough. I'm ok with this, but some mathematicians likely are not

[leanprover-community-bot-assistant]

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