nhds_cons — Mathlib

English

The neighborhood of a cons equals the product of the neighborhoods mapped by List.cons.

Русский

Окрестность конструкторa cons равна произведению окрестностей, отображённых через List.cons.

LaTeX

$$$ \mathcal{N}(a::l) = \operatorname{List}.map(\operatorname{List}.cons) (\mathcal{N}(a)) \;\otimes\; \mathcal{N}(l) $$$

Lean4

theorem nhds_cons (a : α) (l : List α) : 𝓝 (a :: l) = List.cons <$> 𝓝 a <*> 𝓝 l := by
  rw [nhds_list, List.traverse_cons _, ← nhds_list]

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