Theorem ENNReal.exists_ne_top

Modification history

2025-10-05 07:59
Mathlib/Data/ENNReal/Basic.lean
feat: {forall,exists}_ne_{top,bot} (#30208) …
Modified ENNReal.exists_ne_topView on Github →
2024-06-09 14:51
Mathlib/Data/ENNReal/Basic.lean
chore(*): drop some long-deprecated theorems (#13619)
Modified ENNReal.exists_ne_topView on Github →
2024-01-08 13:15
Mathlib/Data/Real/ENNReal.lean
chore(*): use `∃ x ∈ s, p x` instead of `∃ x (_ : x ∈ s), p x` (#9326) …
Modified ENNReal.exists_ne_topView on Github →
2023-02-27 08:10
Mathlib/Data/Real/ENNReal.lean
feat: port Data.Real.ENNReal (#2388) …
Added ENNReal.exists_ne_topView on Github →