Theorems · Theorem · order theory
Filter.limsup_congr
∀ {β : Type u_2} {α : Type u_6} [inst : ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β},
(∀ᶠ (a : α) in f, u a = v a) → Filter.limsup u f = Filter.limsup v f- Defined in
- Mathlib.Order.LiminfLimsup
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext, Quot.sound
- Assumes
- ConditionallyCompleteLattice
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.
- Setproof · cited by 53,352
- Filterstatement and proof · cited by 8,121
- Set.ofPredproof · cited by 6,101
- Filter.Eventuallystatement and proof · cited by 3,134
- InfSet.sInfproof · cited by 935
- Filter.mapproof · cited by 819
- Filter.Eventually.monoproof · cited by 646
- ConditionallyCompleteLatticestatement and proof · cited by 364
- Filter.limsupstatement and proof · cited by 226
- InfSetproof · cited by 145
- Filter.eventually_congrproof · cited by 20
- Filter.limsup_eqproof · cited by 4
Cited by20
Results whose statement or proof uses this declaration.
- Filter.liminf_congrproof · cited by 14
- LinearGrowth.linearGrowthSup_botproof · cited by 6
- Filter.blimsup_congrproof · cited by 4
- essSup_congr_aeproof · cited by 4
- limsup_eq_botproof · cited by 3
- ENNReal.limsup_const_mulproof · cited by 3
- ProbabilityTheory.Kernel.setIntegral_density_of_measurableSetproof · cited by 2
- ExpGrowth.expGrowthSup_supproof · cited by 2
- ENNReal.ofReal_limsup_toRealproof · cited by 1
- LinearGrowth.linearGrowthSup_add_leproof · cited by 1
- ExpGrowth.le_expGrowthSup_mulproof · cited by 1
- LinearGrowth.linearGrowthSup_supproof · cited by 1