Theorems · Theorem · order theory

Filter.limsSup_le_of_le

∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {f : Filter α} {a : α},
  autoParam (Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) f) Filter.limsSup_le_of_le._auto_1 →
    (∀ᶠ (n : α) in f, n ≤ a) → f.limsSup ≤ a

Defined in: Mathlib.Order.LiminfLimsup
Cited by: 4 results in Mathlib
Foundations: Depth 11 from the axioms · uses no axioms
Assumes: ConditionallyCompleteLattice

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Filterstatement and proof · cited by 8,121
Filter.Eventuallystatement and proof · cited by 3,134
ConditionallyCompleteLatticestatement and proof · cited by 364
csInf_leproof · cited by 51
Filter.IsCoboundedstatement and proof · cited by 42
Filter.limsSupstatement · cited by 29

Cited by4

Results whose statement or proof uses this declaration.

Filter.frequently_lt_of_lt_limsupproof · cited by 10
ProbabilityTheory.Kernel.indep_biSup_limsupproof · cited by 3
Filter.frequently_lt_of_lt_limsSupproof · cited by 3
GaloisConnection.l_limsup_leproof · cited by 1