frequently_nhdsWithin_iff — Mathlib

English

A frequently vanishing behavior within s is equivalent to frequently vanishing behavior at a with s-membership included.

Русский

Часто встречающееся поведение внутри s эквивалентно часто встречающемуся поведению в точке a с включением членства в s.

LaTeX

$$frequently_inf_principal.trans (by simp)$$

Lean4

theorem frequently_nhdsWithin_iff {z : α} {s : Set α} {p : α → Prop} :
    (∃ᶠ x in 𝓝[s] z, p x) ↔ ∃ᶠ x in 𝓝 z, p x ∧ x ∈ s :=
  frequently_inf_principal.trans <| by simp only [and_comm]

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