eventually_atTop

Mathlib.Order.Filter.AtTopBot.Basic

URI: https://scilib.ai/kg/mathlib#Filter.eventually_atTop

English

(∀ᶠ x ∈ atTop, p x) is equivalent to ∃ a, ∀ b ≥ a, p b.

Русский

Сходимость к частоте на atTop эквивалентна существованию a, такого что ∀ b ≥ a, выполняется p b.

LaTeX

$$$ (\\forall^{\\mathrm{e}} x \\in \\mathrm{atTop}, p x) \\iff \\exists a, \\forall b \\ge a, p b $$$

Lean4

@[simp]
theorem eventually_atTop : (∀ᶠ x in atTop, p x) ↔ ∃ a, ∀ b ≥ a, p b :=
  mem_atTop_sets

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru