feat(Mathlib/Data/Finite/Option): option type is finite iff type is finite by AlexBrodbelt · Pull Request #39567 · leanprover-community/mathlib4

AlexBrodbelt · 2026-05-19T09:29:40Z

Option type is finite if and only if the type is finite.

This is an intermediate result to proving that if the GroupWithZero is (in)finite then the Units are (in)finite.

…inite

github-actions · 2026-05-19T09:29:55Z

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-05-19T09:31:02Z

PR summary e6a4467394

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Data.Finite.Option` (new file)	627

Declarations diff (regex)

+ Option.finite_iff
+ Option.infinite_iff

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit e6a4467).

+2 new declarations
−0 removed declarations

+Option.finite_iff
+Option.infinite_iff

No changes to strong technical debt.
No changes to weak technical debt.

Current commit e6a4467394
Reference commit 8e30cac82f

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py 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).

ADedecker · 2026-08-13T00:17:45Z

Hi @AlexBrodbelt, are you still working on this? No pressure of course!

felixpernegger

Maybe also include the same thing for Infinite?

Also, would proving the result for Countable and Uncountable here cause issues?

felixpernegger · 2026-08-19T18:17:03Z

+-/
+module
+
+public import Mathlib.Data.Finite.Defs


Suggested change

public import Mathlib.Data.Finite.Defs

public import Mathlib.Data.Finite.Defs

The change you are proposing leaves it unchanged?

no; it adds an empty line between public and private imports; which is the convention

ah okay, will keep that in mind. thanks!

Regarding the analogous Countable and Uncountable results. Maybe a new file or even folder should be made? For now I will push including the Infinite case and work on the remaining cases on another branch

yeah maybe, but at the same time 30 lines files are a bit unfortunate imo

themathqueen · 2026-10-01T17:10:23Z

Please "resolve conversation" when you've addressed the comments, and then when you're ready for another review please comment -awaiting-review :)

Also, you'll probably need to merge master in order to fix the CI error.

plp127 · 2026-10-02T00:01:24Z

+
+public section
+
+/-- `Option α`  is finite if and only if the underlying type `α`is finite. -/


Suggested change

/-- `Option α` is finite if and only if the underlying type `α`is finite. -/

/-- `Option α` is finite if and only if the underlying type `α` is finite. -/

…te/Option

AlexBrodbelt · 2026-10-02T12:44:38Z

-awaiting-author

themathqueen

I think you should probably move this file to Basic/Finite?

themathqueen · 2026-10-02T12:55:23Z

+/-- `Option α` is infinite if and only if the underlying type `α` is infinite. -/
+@[simp]
+theorem Option.infinite_iff {α : Type*} : Infinite (Option α) ↔ Infinite α := by
+  rw [← not_finite_iff_infinite, ← not_finite_iff_infinite, Option.finite_iff]


Suggested change

rw [← not_finite_iff_infinite, ← not_finite_iff_infinite, Option.finite_iff]

simp [← not_finite_iff_infinite]

themathqueen · 2026-10-02T12:56:00Z

+  mp
+  | @Finite.intro _ 0 e => (e none).elim0
+  | @Finite.intro _ (n + 1) e => ⟨(e.trans (finSuccEquiv n)).removeNone⟩


Suggested change

mp

| @Finite.intro _ 0 e => (e none).elim0

| @Finite.intro _ (n + 1) e => ⟨(e.trans (finSuccEquiv n)).removeNone⟩

mp _ := .of_injective _ (Option.some_injective α)

themathqueen · 2026-10-02T13:03:59Z

Or actually, why not just add these results to Mathlib/Data/Fintype/Option?

AlexBrodbelt added 3 commits May 18, 2026 18:47

added finiteness conditions to option type

38fe3ed

feat(Mathlib/Data/Finite/Option): option type is finite iff type is f…

53ac572

…inite

remove min import command

3ca377b

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 May 19, 2026

github-actions Bot added the t-data Data (lists, quotients, numbers, etc) label May 19, 2026

AlexBrodbelt mentioned this pull request May 19, 2026

feat(Mathlib/Data/Finite/Subtype): Subtype of elements not equal to a term is finite iff type is finite #39568

Open

1 task

AlexBrodbelt added 2 commits May 19, 2026 11:44

add new file to Mathlib.lean

99baf79

added docstrings and comments to files

a88c8cc

themathqueen reviewed May 19, 2026

View reviewed changes

Comment thread Mathlib/Data/Finite/Option.lean Outdated

Comment thread Mathlib/Data/Finite/Option.lean Outdated

Comment thread Mathlib/Data/Finite/Option.lean Outdated

Comment thread Mathlib/Data/Finite/Option.lean Outdated

AlexBrodbelt mentioned this pull request May 19, 2026

feat(Mathlib/Data/Finite/Units): Units are (in)finite if type is (in)finite #39569

Open

2 tasks

follow modifications from review

7531e4e

plp127 reviewed May 19, 2026

View reviewed changes

Comment thread Mathlib/Data/Finite/Option.lean Outdated

modify imports

a5cd43a

themathqueen reviewed Jun 2, 2026

View reviewed changes

Comment thread Mathlib/Data/Finite/Option.lean Outdated

themathqueen reviewed Jun 2, 2026

View reviewed changes

Comment thread Mathlib/Data/Finite/Option.lean

mathlib-triage Bot assigned joneugster Jun 5, 2026

mathlib-triage Bot assigned TwoFX and unassigned joneugster Jun 21, 2026

mathlib-triage Bot assigned eric-wieser and unassigned TwoFX Jul 16, 2026

mathlib-triage Bot unassigned eric-wieser Aug 8, 2026

ADedecker added the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Aug 13, 2026

felixpernegger reviewed Aug 19, 2026

View reviewed changes

fix comments and follow import conventions

821be84

plp127 reviewed Oct 2, 2026

View reviewed changes

Merge remote-tracking branch 'upstream/master' into AlexBrodbelt/Fini…

953a74b

…te/Option

AlexBrodbelt added 2 commits October 2, 2026 11:02

fix imports

30a238b

fix comments

e6a4467

github-actions Bot removed the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Oct 2, 2026

themathqueen reviewed Oct 2, 2026

View reviewed changes

themathqueen added the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Oct 2, 2026

	public import Mathlib.Data.Finite.Defs
	public import Mathlib.Data.Finite.Defs


		public section

		/-- `Option α` is finite if and only if the underlying type `α`is finite. -/

	rw [← not_finite_iff_infinite, ← not_finite_iff_infinite, Option.finite_iff]
	simp [← not_finite_iff_infinite]

Conversation

AlexBrodbelt commented May 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented May 19, 2026

Welcome new contributor!

Uh oh!

github-actions Bot commented May 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary e6a4467394

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ADedecker commented Aug 13, 2026

Uh oh!

felixpernegger left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

AlexBrodbelt Oct 1, 2026 • 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!

Choose a reason for hiding this comment

Uh oh!

themathqueen commented Oct 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

AlexBrodbelt commented Oct 2, 2026

Uh oh!

themathqueen left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

themathqueen commented Oct 2, 2026

Uh oh!

This branch has not been deployed

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants

AlexBrodbelt commented May 19, 2026 •

edited

Loading

github-actions Bot commented May 19, 2026 •

edited

Loading

AlexBrodbelt Oct 1, 2026 •

edited

Loading

themathqueen commented Oct 1, 2026 •

edited

Loading