ENNReal.exists_biSup_le_enorm_add_eps

lemma exists_biSup_le_enorm_add_eps    {f : ι → E} {ε : ℝ≥0} (εpos : 0 < ε) (hs : s.Nonempty) (hf : IsBounded (f '' s)) :    ∃ x ∈ s, ⨆ z ∈ s, ‖f z‖ₑ ≤ ‖f x‖ₑ + ε := by  by_contra! H  have M : ⨆ z ∈ s, ‖f z‖ₑ + ε ≤ ⨆ z ∈ s, ‖f z‖ₑ := by    simpa only [iSup_le_iff] using fun i hi ↦ (H i hi).le  have nt : ⨆ z ∈ s, ‖f z‖ₑ ≠ ⊤ := by -- boundedness of `f` used here    rw [ne_eq, iSup₂_eq_top]; push Not    obtain ⟨C, pC, hC⟩ := hf.exists_pos_norm_le; lift C to ℝ≥0 using pC.le    simp_rw [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at hC    exact ⟨C, coe_lt_top, mod_cast hC⟩  obtain ⟨B, eB⟩ : ∃ B : ℝ≥0, ⨆ z ∈ s, ‖f z‖ₑ = B := Option.ne_none_iff_exists'.mp nt  rw [← biSup_add hs, eB] at M  norm_cast at M  exact lt_irrefl _ (M.trans_lt (lt_add_of_pos_right B εpos))