feat(SetTheory/Ordinal/FixedPointApproximants): add zero and limit lemmas for approximants by NoneMore · Pull Request #37375 · leanprover-community/mathlib4

NoneMore · 2026-03-30T14:41:13Z

Add helper lemmas lfpApprox_zero, lfpApprox_limit, and the corresponding gfpApprox lemmas by duality.

…mmas for approximants Add `lfpApprox_zero`, `lfpApprox_limit`, and the corresponding `gfpApprox` lemmas by duality.

github-actions · 2026-03-30T14:41:25Z

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

github-actions · 2026-03-30T14:42:19Z

PR summary 5ccfc60402

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ apply_lfpApprox_le_lfpApprox_of_lt
+ gfpApprox_le_apply_gfpApprox_of_lt
+ gfpApprox_of_isSuccLimit
+ gfpApprox_zero
+ lfpApprox_of_isSuccLimit
+ lfpApprox_zero

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

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean

vihdzp · 2026-03-30T16:57:59Z

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean

+    lfpApprox f x a = ⨆ b : Set.Iio a, lfpApprox f x b := by
+  refine le_antisymm ?_ (iSup_le fun b => lfpApprox_monotone f x b.2.le)
+  rw [lfpApprox]
+  simp only [exists_prop, Set.union_singleton, sSup_insert, sup_le_iff, sSup_le_iff,


I notice only now that the definitions of lfpApprox and gfpApprox aren't simp normal. Nothing you need to do in this PR; I'll open a new one to amend that.

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean

vihdzp · 2026-03-30T18:05:55Z

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean

+    · nth_rw 2 [lfpApprox]
+      exact le_sSup <| Or.inl ⟨b, lt_add_one b, rfl⟩


I think there's a more general result we can extract: f (lfpApprox f x a) ≤ lfpApprox f x b when a < b.

Yes. I also found that this lemma can be used to strengthen lfpApprox_eq_of_mem_fixedPoints by removing the x ≤ f x hypothesis.

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean

name changes Co-authored-by: Violeta Hernández Palacios <[email protected]>

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean

vihdzp

Otherwise LGTM. lfpApprox_add_one can be golfed further, but I completely rewrite it in #37383 anyways, so it doesn't really matter.

Please merge master to fix the build failure!

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean

remove parentheses Co-authored-by: Violeta Hernández Palacios <[email protected]>

NoneMore · 2026-03-31T15:50:43Z

Thanks for the review, particularly the style suggestions! I have to say that I'm bad at this.

YaelDillies

Thanks!

maintainer delegate

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean

github-actions · 2026-04-01T15:04:32Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

feat(SetTheory/Ordinal/FixedPointApproximants): add zero and limit le…

c636ecb

…mmas for approximants Add `lfpApprox_zero`, `lfpApprox_limit`, and the corresponding `gfpApprox` lemmas by duality.

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Mar 30, 2026

github-actions bot added the t-set-theory Set theory label Mar 30, 2026

NoneMore mentioned this pull request Mar 30, 2026

feat(Topology/CantorBendixson): add iterated derived sets and perfect kernel #37376

Open

2 tasks

vihdzp reviewed Mar 30, 2026

View reviewed changes

NoneMore added 2 commits March 31, 2026 13:46

refactor: add and reuse helper lemmas

3a1ac44

golf

be15e96

vihdzp reviewed Mar 31, 2026

View reviewed changes

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean Outdated Show resolved Hide resolved

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean Outdated Show resolved Hide resolved

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean Outdated Show resolved Hide resolved

NoneMore and others added 2 commits March 31, 2026 14:28

Apply suggestions from code review

6fa5e0d

name changes Co-authored-by: Violeta Hernández Palacios <[email protected]>

fix rename

c393046

vihdzp reviewed Mar 31, 2026

View reviewed changes

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean Outdated Show resolved Hide resolved

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean Outdated Show resolved Hide resolved

golf

8a17349

vihdzp reviewed Mar 31, 2026

View reviewed changes

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean Outdated Show resolved Hide resolved

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean Outdated Show resolved Hide resolved

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean Outdated Show resolved Hide resolved

style changes

eaaf6a3

vihdzp approved these changes Mar 31, 2026

View reviewed changes

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean Outdated Show resolved Hide resolved

vihdzp requested a review from YaelDillies March 31, 2026 07:45

NoneMore and others added 3 commits March 31, 2026 18:08

Apply suggestions from code review

3878b5d

remove parentheses Co-authored-by: Violeta Hernández Palacios <[email protected]>

Merge branch 'master' into gfpApprox

b194ac4

fix lint

130be52

YaelDillies approved these changes Apr 1, 2026

View reviewed changes

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean Outdated Show resolved Hide resolved

mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 1, 2026

NoneMore added 2 commits April 1, 2026 23:13

style change

9de4e69

style change

7b79498

		· nth_rw 2 [lfpApprox]
		exact le_sSup <\| Or.inl ⟨b, lt_add_one b, rfl⟩

Conversation

NoneMore commented Mar 30, 2026

Uh oh!

github-actions bot commented Mar 30, 2026

Welcome new contributor!

Uh oh!

github-actions bot commented Mar 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 5ccfc60402

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

vihdzp Mar 30, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

vihdzp Mar 30, 2026

Choose a reason for hiding this comment

Uh oh!

NoneMore Mar 31, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

vihdzp left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

NoneMore commented Mar 31, 2026

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

github-actions bot commented Apr 1, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

github-actions bot commented Mar 30, 2026 •

edited

Loading

vihdzp left a comment •

edited

Loading