From ac2a85d87e0075b125bb2e6349fa6cb87ec1796a Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Mon, 12 Feb 2024 20:58:15 +0100 Subject: [PATCH] rename --- Mathlib/Data/Set/Intervals/Disjoint.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/Set/Intervals/Disjoint.lean b/Mathlib/Data/Set/Intervals/Disjoint.lean index e0c1e5b5af8be..5791ca2f7c056 100644 --- a/Mathlib/Data/Set/Intervals/Disjoint.lean +++ b/Mathlib/Data/Set/Intervals/Disjoint.lean @@ -266,7 +266,7 @@ theorem iUnion_Iic_of_not_bddAbove_range (hf : ¬ BddAbove (range f)) : ⋃ i, I theorem iInter_Iic_eq_iff : ⋂ i, Iic (f i) = ∅ ↔ ¬ BddBelow (range f) := by simp [not_bddBelow_iff, Set.eq_empty_iff_forall_not_mem] -theorem iInter_Iio_eq_of_not_bddBelow_range (hf : ¬ BddBelow (range f)) : ⋂ i, Iio (f i) = ∅ := by +theorem iInter_Iio_eq_empty_iff (hf : ¬ BddBelow (range f)) : ⋂ i, Iio (f i) = ∅ := by refine' eq_empty_of_subset_empty _ rw [← iInter_Iic_eq_iff.mpr hf] gcongr