nhds_bind_nhds — Mathlib

English

The neighborhood filter at x, bound by itself, equals the neighborhood filter at x: (𝓝 x).bind 𝓝 x = 𝓝 x.

Русский

Фильтр окрестностей в x, связанный сам с собой, равен фильтру окрестностей в x: (𝓝 x).bind 𝓝 x = 𝓝 x.

LaTeX

$$$(\\mathcal N_x).bind(\\mathcal N_x) = \\mathcal N_x.$$$

Lean4

@[simp]
theorem nhds_bind_nhds : (𝓝 x).bind 𝓝 = 𝓝 x :=
  Filter.ext fun _ => eventually_eventually_nhds

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