cast_continuous — Mathlib

English

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

Русский

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

LaTeX

$$$\operatorname{Continuous}(\operatorname{Int.cast} : \mathbb{Z} \to R)$$$

Lean4

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

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