frequently_inf_principal — Mathlib

English

For a filter f and a subset s, frequent on the infimum with the principal filter on s is equivalent to frequent on f with p holding when x ∈ s.

Русский

Для фильтра f и множества s частотность в пересечении f ⊓ 𝓟s эквивалентна частотности в f при условии x ∈ s и p(x).

LaTeX

$$$\\left(\\existsᶠ x\\in f \\inf 𝓟 s,\\ p(x)\\right) \\iff \\existsᶠ x\\in f,\\ x\\in s \\land p(x)$$$

Lean4

theorem frequently_inf_principal {f : Filter α} {s : Set α} {p : α → Prop} :
    (∃ᶠ x in f ⊓ 𝓟 s, p x) ↔ ∃ᶠ x in f, x ∈ s ∧ p x := by
  simp only [Filter.Frequently, eventually_inf_principal, not_and]

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