eventually_iff_all_subsets — Mathlib

English

An eventual statement p x holds iff it holds eventually on every subset of α.

Русский

Утверждение p x выполняется поздно тогда и только тогда, когда оно выполняется поздно на любом подмножестве α.

LaTeX

$$$ (\forall^\infty x \in f,\ p x) \leftrightarrow \forall (s : Set α), \forall^\infty x \in f, x \in s \rightarrow p x $$$

Lean4

theorem eventually_iff_all_subsets {f : Filter α} {p : α → Prop} :
    (∀ᶠ x in f, p x) ↔ ∀ (s : Set α), ∀ᶠ x in f, x ∈ s → p x
    where
  mp h _ := by filter_upwards [h] with _ pa _ using pa
  mpr h := by filter_upwards [h univ] with _ pa using pa (by simp)

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