Theorems · Theorem · general topology
le_liminf_mul
∀ {ι : 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 f * Filter.liminf v f ≤ Filter.liminf (u * v) f- Cited by
- 0 results in Mathlib
- Foundations
- Depth 117 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.univ_mem'proof · cited by 1,672
- Filter.mp_memproof · cited by 1,537
- Filter.NeBotstatement and proof · cited by 853
- LT.lt.trans_leproof · cited by 678
- 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
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.