Theorems · Theorem · general topology
ENNReal.liminf_const_sub
∀ {ι : Type u_4} (F : Filter ι) [F.NeBot] (f : ι → ENNReal) {c : ENNReal},
c ≠ ⊤ → Filter.liminf (fun i => c - f i) F = c - Filter.limsup f F- Cited by
- 0 results in Mathlib
- Foundations
- Depth 134 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Filter.NeBot
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement and proof · cited by 9,879
- Top.topstatement and proof · cited by 9,680
- Filterstatement and proof · cited by 8,121
- Filter.NeBotstatement and proof · cited by 853
- Continuous.continuousAtproof · cited by 297
- Filter.limsupstatement · cited by 226
- Filter.liminfstatement · cited by 198
- Filter.isBounded_le_of_topproof · cited by 75
- Filter.isCobounded_le_of_botproof · cited by 58
- tsub_le_tsub_leftproof · cited by 15
- Antitone.map_limsSup_of_continuousAtproof · cited by 6
- ENNReal.continuous_sub_leftproof · cited by 5
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.