continuous_one — Mathlib

English

If M is a topological space with a unity, then the constant map sending every x to 1 in M is continuous.

Русский

Пусть M — топологическое пространство с единицей. Тогда константное отображение x ↦ 1 из X в M непрерывно.

LaTeX

$$$\text{Continuous}(1 : X \to M)$$$

Lean4

@[to_additive (attr := continuity, fun_prop)]
theorem continuous_one [TopologicalSpace M] [One M] : Continuous (1 : X → M) :=
  @continuous_const _ _ _ _ 1

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