Skip to content

Commit d00cab5

Browse files
committed
fix(Topology/Baire/Lemmas): fix index type in isMeagre_iUnion (#30141)
The index set ι needs to be of type Sort* instead of type Type* in isMeagre_iUnion otherwise I get the following message when I try to use it: typeclass instance problem is stuck, it is often due to metavariables Countable ?m.27
1 parent 27fa680 commit d00cab5

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Mathlib/Topology/GDelta/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -232,7 +232,7 @@ lemma IsMeagre.union {s t : Set X} (hs : IsMeagre s) (ht : IsMeagre t) : IsMeagr
232232
exact inter_mem hs ht
233233

234234
/-- A countable union of meagre sets is meagre. -/
235-
lemma isMeagre_iUnion [Countable ι] {f : ι → Set X} (hs : ∀ i, IsMeagre (f i)) :
235+
lemma isMeagre_iUnion [Countable ι'] {f : ι' → Set X} (hs : ∀ i, IsMeagre (f i)) :
236236
IsMeagre (⋃ i, f i) := by
237237
rw [IsMeagre, compl_iUnion]
238238
exact countable_iInter_mem.mpr hs

0 commit comments

Comments
 (0)