instTopologicalSpace — Mathlib

English

The map p ↦ p.fst ::ᵥ p.snd (i.e., cons-ing an element to a vector) is continuous from α × Vector α n to Vector α (n+1).

Русский

Отображение, которое приставляет элемент слева к вектору, непрерывно с точки зрения топологии α × Vector α n в Vector α (n+1).

LaTeX

$$$\\\\forall {\\\\alpha}, [TopologicalSpace(\\\\alpha)], {n}, {a}, {l}, \\\\text{Tendsto}(\\\\lambda p: \\\\alpha \\\\times \\\\text{Vector}(\\\\alpha,n), p.1 ::ᵥ p.2) \\\\rightarrow \\\\mathcal{N}(a ::ᵥ l)$$$

Lean4

instance (n : ℕ) : TopologicalSpace (Vector α n) := by unfold Vector; infer_instance

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