frequently_atTop' — Mathlib

English

NoMaxOrder α implies a dual frequent statement for atTop with Ioi: (∃ᶠ x ∈ atTop, p x) ↔ ∀ a, ∃ b > a, p b.

Русский

При отсутствии максимума в α справедливо частотное свойство для atTop с Ioi: (∃ᶠ x ∈ atTop, p x) ↔ ∀ a, ∃ b > a, p b.

LaTeX

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

Lean4

theorem frequently_atTop' [NoMaxOrder α] : (∃ᶠ x in atTop, p x) ↔ ∀ a, ∃ b > a, p b :=
  atTop_basis_Ioi.frequently_iff.trans <| by simp

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