feat: EReal.forall, EReal.exists (#18301)

Mathlib/Data/Real/EReal.lean

@@ -132,6 +132,14 @@ protected def rec {C : EReal → Sort*} (h_bot : C ⊥) (h_real : ∀ a : ℝ, C
   | (a : ℝ) => h_real a
   | ⊤ => h_top
 
+protected lemma «forall» {p : EReal → Prop} : (∀ r, p r) ↔ p ⊥ ∧ p ⊤ ∧ ∀ r : ℝ, p r where
+  mp h := ⟨h _, h _, fun _ ↦ h _⟩
+  mpr h := EReal.rec h.1 h.2.2 h.2.1
+
+protected lemma «exists» {p : EReal → Prop} : (∃ r, p r) ↔ p ⊥ ∨ p ⊤ ∨ ∃ r : ℝ, p r where
+  mp := by rintro ⟨r, hr⟩; cases r <;> aesop
+  mpr := by rintro (h | h | ⟨r, hr⟩) <;> exact ⟨_, ‹_›⟩
+
 /-- The multiplication on `EReal`. Our definition satisfies `0 * x = x * 0 = 0` for any `x`, and
 picks the only sensible value elsewhere. -/
 protected def mul : EReal → EReal → EReal