rename

leanprover-community · Feb 12, 2024 · ac2a85d · ac2a85d
1 parent 49ac817
commit ac2a85d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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