From e0404bcc1ff05315d5b8230f2216e30d33016742 Mon Sep 17 00:00:00 2001 From: kkytola Date: Sat, 25 Nov 2023 15:15:58 +0000 Subject: [PATCH] chore: Fix universe (misprint in Portmanteau.lean). (#8620) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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! --- Mathlib/MeasureTheory/Measure/Portmanteau.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/MeasureTheory/Measure/Portmanteau.lean b/Mathlib/MeasureTheory/Measure/Portmanteau.lean index 16f7861445864b..20e1b1dc848f0b 100644 --- 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)