nhds_bind_nhdsWithin — Mathlib

English

The neighborhood of a with a bind of neighborhoods within s collapses to the s-neighborhood: (nhds a).bind (nhdsWithin · s) = nhdsWithin a s.

Русский

Для точки a и множества s пересечение образует соседство внутри s: (nhds a).bind (nhdsWithin · s) = nhdsWithin a s.

LaTeX

$$$ (𝓝 a) \bind (\mathcal{N}[s] ) = 𝓝[s] a$$$

Lean4

@[simp]
theorem nhds_bind_nhdsWithin {a : α} {s : Set α} : ((𝓝 a).bind fun x => 𝓝[s] x) = 𝓝[s] a :=
  bind_inf_principal.trans <| congr_arg₂ _ nhds_bind_nhds rfl

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