frequently_nhds_subtype_iff — Mathlib

English

For s ⊆ α, a ∈ s as a subtype, P : α → Prop, the frequent occurrence along nhds a in the ambient space is equivalent to frequent occurrence along nhds within the subtype.

Русский

Для s ⊆ α, a ∈ s как элемент подтипа, P: α → Prop, частота выполнения на nhds эквивалентна частоте на nhds внутри подтипа.

LaTeX

$$$ (\\exists^\\infty x : s in 𝓝 a, P x) \\iff \\ (\\exists^\\infty x in 𝓝[s] a, P x) $$$

Lean4

theorem frequently_nhds_subtype_iff (s : Set α) (a : s) (P : α → Prop) : (∃ᶠ x : s in 𝓝 a, P x) ↔ ∃ᶠ x in 𝓝[s] a, P x :=
  eventually_nhds_subtype_iff s a (¬P ·) |>.not

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