Skip to content

Commit 39e9664

Browse files
kim-emclaude
andcommitted
fix: update named argument b₁ → a₁ for GaloisConnection.u_inf
The `@[to_dual]` attribute generates `u_inf` from `l_sup`, which uses `a₁`/`a₂` as parameter names instead of the old `b₁`/`b₂`. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
1 parent 0ac9d3f commit 39e9664

File tree

2 files changed

+3
-3
lines changed

2 files changed

+3
-3
lines changed

Mathlib/Algebra/Module/Torsion/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -427,7 +427,7 @@ theorem supIndep_torsionBySet_ideal (hp : (S : Set ι).Pairwise fun i j => p i
427427
rw [disjoint_iff, Finset.sup_eq_iSup,
428428
iSup_torsionBySet_ideal_eq_torsionBySet_iInf fun i hi j hj ij => hp (hT hi) (hT hj) ij]
429429
have := GaloisConnection.u_inf
430-
(b₁ := OrderDual.toDual (p i)) (b₂ := OrderDual.toDual (⨅ i ∈ T, p i)) (torsion_gc R M)
430+
(a₁ := OrderDual.toDual (p i)) (a₂ := OrderDual.toDual (⨅ i ∈ T, p i)) (torsion_gc R M)
431431
dsimp at this ⊢
432432
rw [← this, Ideal.sup_iInf_eq_top, top_coe, torsionBySet_univ]
433433
intro j hj; apply hp hi (hT hj); rintro rfl; exact hiT hj

Mathlib/Topology/Order.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -668,10 +668,10 @@ theorem nhds_sInf {s : Set (TopologicalSpace α)} {a : α} :
668668
@nhds α (sInf s) a = ⨅ t ∈ s, @nhds α t a :=
669669
(gc_nhds a).u_sInf
670670

671-
-- Porting note: type error without `b₁ := t₁`
671+
-- Porting note: type error without `a₁ := t₁`
672672
theorem nhds_inf {t₁ t₂ : TopologicalSpace α} {a : α} :
673673
@nhds α (t₁ ⊓ t₂) a = @nhds α t₁ a ⊓ @nhds α t₂ a :=
674-
(gc_nhds a).u_inf (b₁ := t₁)
674+
(gc_nhds a).u_inf (a₁ := t₁)
675675

676676
theorem nhds_top {a : α} : @nhds α ⊤ a = ⊤ :=
677677
(gc_nhds a).u_top

0 commit comments

Comments
 (0)