liminf_le_of_frequently_le' — Mathlib

English

If there exists a frequently (infinitely often) a in f such that u(a) ≤ x, then liminf u f ≤ x.

Русский

Если существует частотное (бесконечно часто встречающееся) a в f, такое что u(a) ≤ x, то liminf u f ≤ x.

LaTeX

$$$\\exists^{\\text{ frequently }} a \\in f:\\ u(a) \\le x \\quad\\Rightarrow\\quad \\liminf u f \\le x$$$

Lean4

theorem liminf_le_of_frequently_le' {α β} [CompleteLattice β] {f : Filter α} {u : α → β} {x : β}
    (h : ∃ᶠ a in f, u a ≤ x) : liminf u f ≤ x := by
  rw [liminf_eq]
  refine sSup_le fun b hb => ?_
  have hbx : ∃ᶠ _ in f, b ≤ x := by
    revert h
    rw [← not_imp_not, not_frequently, not_frequently]
    exact fun h => hb.mp (h.mono fun a hbx hba hax => hbx (hba.trans hax))
  exact hbx.exists.choose_spec

Похожие утверждения