forall_mem — Mathlib

English

If a property p holds eventually with respect to f and s is contained in f, then p holds for all elements of s.

Русский

Если p выполняется часто относительно f и s ≤ f, то ∀ x ∈ s, p x.

LaTeX

$$$ (\forall^\infty x \in f, P x) \land (hf : 𝓟 s \le f) \rightarrow \forall x \in s, P x $$$

Lean4

theorem forall_mem {α : Type*} {f : Filter α} {s : Set α} {P : α → Prop} (hP : ∀ᶠ x in f, P x) (hf : 𝓟 s ≤ f) :
    ∀ x ∈ s, P x :=
  Filter.eventually_principal.mp (hP.filter_mono hf)

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