eventually_nhds_subtype_iff — Mathlib

English

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

Русский

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

LaTeX

$$$ (∀ᶠ x : s in 𝓝 a, P x) \iff ∀ᶠ x in 𝓝[s] a, P x $$$

Lean4

theorem eventually_nhds_subtype_iff (s : Set α) (a : s) (P : α → Prop) : (∀ᶠ x : s in 𝓝 a, P x) ↔ ∀ᶠ x in 𝓝[s] a, P x :=
  preimage_coe_mem_nhds_subtype

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