cast_continuous — Mathlib

English

The natural embedding of the natural numbers into any topological space R is continuous.

Русский

Естественное вложение натуральных чисел в произвольное топологическое пространство R непрерывно.

LaTeX

$$$\operatorname{Continuous}(\operatorname{Nat.cast} : \mathbb{N} \to R)$$$

Lean4

theorem cast_continuous {R : Type*} [NatCast R] [TopologicalSpace R] : Continuous (Nat.cast (R := R)) :=
  continuous_of_discreteTopology

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