[Merged by Bors] - feat(Topology/Algebra/ValuativeTopology): checking `IsValuativeTopology` using any compatible valuation by mathlib-splicebot[bot] · Pull Request #41527 · leanprover-community/mathlib4

mathlib-splicebot · 2026-07-09T08:09:31Z

Add two intro methods of IsValuativeTopology.

This PR was automatically created from PR #36769 by @jjdishere via a review comment by @jjdishere.

Co-authored-by: @faenuccio

…l/ValuativeTopology.lean

github-actions · 2026-07-09T08:10:59Z

PR summary 9de27b745d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

+ of_mem_nhds_iff_vle
+ of_mem_nhds_zero_iff_vle

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

⚠️ The Mathlib cache for this PR's merge-base isn't on the server (typically a bors-batch intermediate that CI never built). Merge master into this PR and push to refresh.

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 9de27b745d
Reference commit e3b73828b0

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

riccardobrasca · 2026-07-09T09:11:26Z

+  refine ⟨fun ⟨γ, hγ⟩ ↦ ⟨γ, subset_of_eq_of_subset (ext (fun a ↦ ⟨?_, ?_⟩)) hγ⟩,
+    fun ⟨γ, hγ⟩ ↦ ⟨γ, subset_of_eq_of_subset (ext (fun a ↦ ⟨?_, ?_⟩)) hγ⟩⟩ <;>
+  first | exact fun ⟨_, ⟨_, h⟩⟩ ↦ by simpa [← h] | exact fun h ↦ ⟨- x + a, ⟨h, by simp⟩⟩


Can we make this a little more readable? Even if it becomes like 5-10 lines I don't think it's a problem.

Still 3 lines, but I guess now it is much better.

…ra-ValuativeRel-ValuativeTopology.lean-70e684a549-i8zprqh

riccardobrasca · 2026-07-10T00:19:46Z

+with the valuative relation, then the underlying topology is valuative. -/
+theorem of_mem_nhds_zero_iff_vle [IsTopologicalAddGroup R]
+    (H : ∀ {s : Set R}, s ∈ 𝓝 0 ↔ ∃ (γ : (ValueGroup₀ (.ofClass v))ˣ),
+    (·) '' {z : R | v.restrict z < γ} ⊆ s) : IsValuativeTopology R := by


Suggested change

(·) '' {z : R | v.restrict z < γ} ⊆ s) : IsValuativeTopology R := by

{z : R | v.restrict z < γ} ⊆ s) : IsValuativeTopology R := by

Maybe I am missing something, but why are you still applying the identity?

Fixed. Thanks!

Also modified previous lemma.

riccardobrasca

Thanks!

bors d+

mathlib-bors · 2026-07-10T00:20:07Z

✌️ mathlib-splicebot[bot] can now approve this pull request until 2026-07-24 00:20 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

⚠️ This delegation only covers changes within Archive/**, Counterexamples/**, docs/**, DownstreamTest/**, Mathlib/**, MathlibTest/**, widget/**, Archive.lean, Counterexamples.lean, docs.lean, Mathlib.lean; an author commit touching anything else will revoke it. Bors also revokes it if a later push changes too many files for it to check the full list — even if it stays within scope.

jjdishere · 2026-07-10T04:56:13Z

Let's see whether I can do this.

bors r+

mathlib-bors · 2026-07-10T04:56:15Z

🔒 Permission denied

An existing reviewer can click here to make jjdishere a reviewer.

jjdishere · 2026-07-10T04:57:39Z

@riccardobrasca
It seems that I am not mathlib-splicebot : /

riccardobrasca · 2026-07-10T04:59:37Z

Hmm, we need to fix this, I always delegate the bot instead of the real author!

bors merge

@jjdishere

…gy` using any compatible valuation (#41527) Add two intro methods of `IsValuativeTopology`. This PR was automatically created from PR #36769 by @jjdishere via a [review comment](#36769 (comment)) by @jjdishere. Co-authored-by: @faenuccio Co-authored-by: jjdishere <107380768+jjdishere@users.noreply.github.com> Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr> Co-authored-by: Jiedong Jiang <emailboxofjjd@163.com>

mathlib-bors · 2026-07-10T05:01:31Z

Build failed:

ci (staging) / Build

Fix if necessary, and then someone with permission can run bors r+ or bors retry.

riccardobrasca · 2026-07-10T05:02:24Z

bors d=@jjdishere

mathlib-bors · 2026-07-10T05:02:26Z

✌️ jjdishere can now approve this pull request until 2026-07-24 05:02 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

⚠️ This delegation only covers changes within Archive/**, Counterexamples/**, docs/**, DownstreamTest/**, Mathlib/**, MathlibTest/**, widget/**, Archive.lean, Counterexamples.lean, docs.lean, Mathlib.lean; an author commit touching anything else will revoke it. Bors also revokes it if a later push changes too many files for it to check the full list — even if it stays within scope.

jjdishere · 2026-07-10T05:12:23Z

bors r+

@jjdishere

…gy` using any compatible valuation (#41527) Add two intro methods of `IsValuativeTopology`. This PR was automatically created from PR #36769 by @jjdishere via a [review comment](#36769 (comment)) by @jjdishere. Co-authored-by: @faenuccio Co-authored-by: jjdishere <107380768+jjdishere@users.noreply.github.com> Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr> Co-authored-by: Jiedong Jiang <emailboxofjjd@163.com>

mathlib-bors · 2026-07-10T05:26:06Z

Pull request successfully merged into master.

Build succeeded:

@jjdishere

…gy` using any compatible valuation (leanprover-community#41527) Add two intro methods of `IsValuativeTopology`. This PR was automatically created from PR leanprover-community#36769 by @jjdishere via a [review comment](leanprover-community#36769 (comment)) by @jjdishere. Co-authored-by: @faenuccio Co-authored-by: jjdishere <107380768+jjdishere@users.noreply.github.com> Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr> Co-authored-by: Jiedong Jiang <emailboxofjjd@163.com>

Automated addition of changes in Mathlib/Topology/Algebra/ValuativeRe…

a64fdcb

…l/ValuativeTopology.lean

github-actions Bot added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Jul 9, 2026

jjdishere changed the title ~~chore(Topology/Algebra/ValuativeRel/ValuativeTopology): automated extraction from #36769~~ feat(Topology/Algebra/ValuativeTopology): checking IsValuativeTopology using any compatible valuation Jul 9, 2026

jjdishere added the t-algebra Algebra (groups, rings, fields, etc) label Jul 9, 2026

jjdishere requested a review from riccardobrasca July 9, 2026 08:17

riccardobrasca reviewed Jul 9, 2026

View reviewed changes

Comment thread Mathlib/Topology/Algebra/ValuativeRel/ValuativeTopology.lean Outdated

riccardobrasca reviewed Jul 9, 2026

View reviewed changes

faenuccio added 2 commits July 9, 2026 18:47

Merge branch 'master' into splice-bot/pr-36769-Mathlib-Topology-Algeb…

4c5fe16

…ra-ValuativeRel-ValuativeTopology.lean-70e684a549-i8zprqh

followed reviewer's suggestion

4abd3d7

riccardobrasca reviewed Jul 10, 2026

View reviewed changes

mathlib-bors Bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jul 10, 2026

jjdishere added 2 commits July 10, 2026 12:51

apply suggestion

755587b

fix

93f4784

mathlib-bors Bot added the ready-to-merge This PR has been sent to bors. label Jul 10, 2026

mathlib-bors Bot added bors-staging This PR is currently being built by bors on the staging branch. awaiting-requeue This PR was on the bors queue but came off after a build failure or other issue. labels Jul 10, 2026

mathlib-bors Bot removed ready-to-merge This PR has been sent to bors. bors-staging This PR is currently being built by bors on the staging branch. labels Jul 10, 2026

fix

9de27b7

mathlib-bors Bot added ready-to-merge This PR has been sent to bors. and removed awaiting-requeue This PR was on the bors queue but came off after a build failure or other issue. labels Jul 10, 2026

mathlib-bors Bot added the bors-staging This PR is currently being built by bors on the staging branch. label Jul 10, 2026

mathlib-bors Bot changed the title ~~feat(Topology/Algebra/ValuativeTopology): checking IsValuativeTopology using any compatible valuation~~ [Merged by Bors] - feat(Topology/Algebra/ValuativeTopology): checking IsValuativeTopology using any compatible valuation Jul 10, 2026

mathlib-bors Bot closed this Jul 10, 2026

mathlib-bors Bot removed the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jul 10, 2026

	(·) '' {z : R \| v.restrict z < γ} ⊆ s) : IsValuativeTopology R := by
	{z : R \| v.restrict z < γ} ⊆ s) : IsValuativeTopology R := by

Uh oh!

Conversation

mathlib-splicebot Bot commented Jul 9, 2026 • edited by jjdishere Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary 9de27b745d

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean -- unavailable)

Uh oh!

Uh oh!

riccardobrasca Jul 9, 2026

Choose a reason for hiding this comment

Uh oh!

faenuccio Jul 9, 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!

riccardobrasca Jul 10, 2026

Choose a reason for hiding this comment

Uh oh!

jjdishere Jul 10, 2026

Choose a reason for hiding this comment

Uh oh!

jjdishere Jul 10, 2026

Choose a reason for hiding this comment

Uh oh!

riccardobrasca left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors Bot commented Jul 10, 2026

Uh oh!

jjdishere commented Jul 10, 2026

Uh oh!

mathlib-bors Bot commented Jul 10, 2026

Uh oh!

jjdishere commented Jul 10, 2026

Uh oh!

riccardobrasca commented Jul 10, 2026

Uh oh!

mathlib-bors Bot commented Jul 10, 2026

Uh oh!

riccardobrasca commented Jul 10, 2026

Uh oh!

mathlib-bors Bot commented Jul 10, 2026

Uh oh!

jjdishere commented Jul 10, 2026

Uh oh!

mathlib-bors Bot commented Jul 10, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

mathlib-splicebot Bot commented Jul 9, 2026 •

edited by jjdishere

Loading

github-actions Bot commented Jul 9, 2026 •

edited

Loading

faenuccio Jul 9, 2026 •

edited

Loading