forall_exists_of_atBot — Mathlib

English

If p holds frequently along atTop, then for every a there exists b ≥ a with p(b).

Русский

Если p выполняется часто по отношению к atTop, то для каждого a существует b ≥ a, такой что p(b).

LaTeX

$$$\\text{Frequently}(p\\,\\text{on atTop}) \\Rightarrow \\forall a\\,\\exists b\\ge a\\, p(b).$$$

Lean4

theorem forall_exists_of_atBot [Preorder α] {p : α → Prop} (h : ∃ᶠ x in atBot, p x) (a : α) : ∃ b ≤ a, p b :=
  Frequently.forall_exists_of_atTop (α := αᵒᵈ) h _

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