chore: Fix universe (misprint in Portmanteau.lean). (#8620)

In my earlier PR #8097 there there was a typo `variable {Ω : Type}` which should have been a universe polymorphic `variable {Ω : Type*}`. This PR fixes 1 character. Apologies!
leanprover-community · Nov 25, 2023 · 1c6e8b5 · 1c6e8b5
1 parent 5ddf761
commit 1c6e8b5
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/MeasureTheory/Measure/Portmanteau.lean b/Mathlib/MeasureTheory/Measure/Portmanteau.lean
@@ -550,7 +550,7 @@ implies
 
 -/
 
-variable {Ω : Type} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω]
+variable {Ω : Type*} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω]
 
 lemma lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure
     {μ : Measure Ω} {μs : ℕ → Measure Ω} {f : Ω → ℝ} (f_cont : Continuous f) (f_nn : 0 ≤ f)