Theorems · Theorem · general topology
liminf_mul_le
∀ {ι : Type u_1} {f : Filter ι} {u v : ι → ℝ} [f.NeBot],
0 ≤ᶠ[f] u →
Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u →
0 ≤ᶠ[f] v →
Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v →
Filter.liminf (u * v) f ≤ Filter.limsup u f * Filter.liminf v f- Cited by
- 0 results in Mathlib
- Foundations
- Depth 118 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.
Cites23
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Filterstatement and proof · cited by 8,121
- LE.le.transproof · cited by 3,151
- LT.lt.leproof · cited by 2,189
- Filter.NeBotstatement and proof · cited by 853
- LE.le.trans_ltproof · cited by 795
- Filter.Eventually.monoproof · cited by 646
- mul_nonnegproof · cited by 397
- Filter.EventuallyLEstatement and proof · cited by 383
- Filter.IsBoundedUnderstatement and proof · cited by 247
- Filter.limsupstatement and proof · cited by 226
- Filter.liminfstatement and proof · cited by 198
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.