[Merged by Bors] - feat(ModelTheory): Formula.iSup and iInf by ChrisHughes24 · Pull Request #21948 · leanprover-community/mathlib4

ChrisHughes24 · 2025-02-16T09:42:35Z

This was a slightly controversial addition discussed in #20175

github-actions · 2025-02-16T09:43:40Z

PR summary 8b2141b23d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ _root_.FirstOrder.Language.Formula.realize_iInf
+ _root_.FirstOrder.Language.Formula.realize_iSup
+ iInf
+ iSup

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

YaelDillies

@awainverse, can you confirm you're happy with this duplication?

Mathlib/ModelTheory/Semantics.lean

Mathlib/ModelTheory/Syntax.lean

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

fpvandoorn

I think this is fine. Could you add a warning to all the 4 definitions that this is an arbitrary formula, and only "well-defined" up to equivalence of formulas (feel free to formulate differently).

bors d+

mathlib-bors · 2025-06-11T09:43:38Z

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

ChrisHughes24 · 2025-06-12T07:33:54Z

bors r+

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

mathlib-bors · 2025-06-12T08:56:39Z

Pull request successfully merged into master.

Build succeeded:

CI Success

* master: (447 commits) chore(Data/Set): move very basic lemmas earlier (leanprover-community#25707) feat: preserve draft status when migrating PRs to fork (leanprover-community#25777) chore(Data/Set/Basic): deprecate lemmas that abuse the `Set α := α → Prop` defeq (leanprover-community#25669) refactor: redefine `ProperCone` as an `abbrev` for `ClosedSubmodule` (leanprover-community#25204) feat: interaction between ContinuousLinearMap.coprod and ContinuousLinearEquiv.prodComm (leanprover-community#25564) fix: outdated docstring (leanprover-community#25717) feat(MeasureTheory): convolution of measures with densities (leanprover-community#25718) feat: make sure that the simp normal form of equiv-like classes pushes `symm` and `trans` to the right (leanprover-community#25604) feat(ModelTheory): Formula.iSup and iInf (leanprover-community#21948) feat(RingTheory/Polynomial/ContentIdeal): the content ideal of a polynomial. (leanprover-community#25333) fix: typo in labels_from_comment.yml (leanprover-community#25727) feat: is{Inducing,Embedding}_prodMkLeft (leanprover-community#25705) feat: check that the mathlib options exist (leanprover-community#25687) feat(Algebra/Group/Even): Add missing lemmas (leanprover-community#20818) refactor: make `Matrix.kroneckerTMulAlgEquiv` heterogeneous (leanprover-community#25693) feat: allow contributors to remove labels with comments (leanprover-community#25723) chore: disable build.yml and bors.yml on forks (leanprover-community#25722) feat: improvements to user_activity_report.py (leanprover-community#25721) chore: update the migration script to check for necessary permissions and prefer ssh if possible (leanprover-community#25701) chore: update the migration script to check for necessary permissions and prefer ssh if possible (leanprover-community#25701) ...

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

ChrisHughes24 added 20 commits December 21, 2024 19:03

refactor(ModelTheory): restate iAlls for a more convenient statement

6b5b5a4

chore(ModelTheory): redefine iInf

970b3c7

undo other changes

db071dc

fix

f06ac2f

fix

217758d

weaken Fintype to Finite

27fee6a

Merge branch 'restateiAlls' into HEAD

80297f0

Merge branch 'restateiInf' into HEAD

20cec1d

feat(ModelTheory): iExsUnique

db81b72

fix

e6009d5

docs

31b859c

Merge remote-tracking branch 'origin/master' into iExsUnique

946ce1e

Merge remote-tracking branch 'origin/master' into iExsUnique

a5a35d4

Merge remote-tracking branch 'origin/master' into iExsUnique

f8f16b9

fix

38256a1

fixes based on comments

96d81b5

Merge remote-tracking branch 'origin/master' into iExsUnique

3e35c9c

feat(ModelTheory): Formula.iInf

0331b14

delete ExsUnique stuff

8b226ad

Merge remote-tracking branch 'origin/master' into iSupiInf

3f9eb93

github-actions bot added the t-logic Logic (model theory, etc) label Feb 16, 2025

This was referenced Feb 16, 2025

refactor(ModelTheory): tidy up proof of Ax-Grothendieck with definable functions #20173

Closed

feat(ModelTheory): definable functions #20180

Closed

YaelDillies reviewed Feb 16, 2025

View reviewed changes

Mathlib/ModelTheory/Semantics.lean Outdated Show resolved Hide resolved

Mathlib/ModelTheory/Semantics.lean Outdated Show resolved Hide resolved

Mathlib/ModelTheory/Syntax.lean Outdated Show resolved Hide resolved

Mathlib/ModelTheory/Syntax.lean Outdated Show resolved Hide resolved

ChrisHughes24 and others added 4 commits February 16, 2025 09:47

Update Mathlib/ModelTheory/Semantics.lean

5a090fc

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/ModelTheory/Semantics.lean

89bc5f6

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/ModelTheory/Syntax.lean

6cb3007

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/ModelTheory/Syntax.lean

fee2db4

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 17, 2025

fpvandoorn reviewed Jun 11, 2025

View reviewed changes

Merge remote-tracking branch 'origin/master' into iSupiInf

39ef9c2

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 12, 2025

docs

f937079

ghost added the ready-to-merge This PR has been sent to bors. label Jun 12, 2025

mathlib-bors bot pushed a commit that referenced this pull request Jun 12, 2025

feat(ModelTheory): Formula.iSup and iInf (#21948)

daf6f1f

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

mathlib-bors bot changed the title ~~feat(ModelTheory): Formula.iSup and iInf~~ [Merged by Bors] - feat(ModelTheory): Formula.iSup and iInf Jun 12, 2025

mathlib-bors bot closed this Jun 12, 2025

mathlib-bors bot deleted the iSupiInf branch June 12, 2025 08:56

pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Jun 15, 2025

feat(ModelTheory): Formula.iSup and iInf (leanprover-community#21948)

d5140b3

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Jun 15, 2025

feat(ModelTheory): Formula.iSup and iInf (leanprover-community#21948)

d4297c3

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

This was referenced Jun 25, 2025

feat(ModelTheory): definable functions #26398

Open

refactor(ModelTheory): tidy up proof of Ax-Grothendieck with definable functions #26399

Open

callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025

feat(ModelTheory): Formula.iSup and iInf (leanprover-community#21948)

db1431b

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(ModelTheory): Formula.iSup and iInf#21948

[Merged by Bors] - feat(ModelTheory): Formula.iSup and iInf#21948
ChrisHughes24 wants to merge 26 commits intomasterfrom
iSupiInf

ChrisHughes24 commented Feb 16, 2025

Uh oh!

github-actions bot commented Feb 16, 2025 •

edited

Loading

Declarations diff

Uh oh!

YaelDillies left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

fpvandoorn left a comment

Uh oh!

mathlib-bors bot commented Jun 11, 2025

Uh oh!

ChrisHughes24 commented Jun 12, 2025

Uh oh!

mathlib-bors bot commented Jun 12, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

ChrisHughes24 commented Feb 16, 2025

Uh oh!

github-actions bot commented Feb 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 8b2141b23d

Import changes for modified files

Declarations diff

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

fpvandoorn left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jun 11, 2025

Uh oh!

ChrisHughes24 commented Jun 12, 2025

Uh oh!

mathlib-bors bot commented Jun 12, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

github-actions bot commented Feb 16, 2025 •

edited

Loading