continuous_coe — Mathlib

English

The natural embedding of the real numbers into the quaternion algebra is continuous; the map x ↦ x viewed as a quaternion is continuous.

Русский

Естественное включение действительных чисел в алгебру кватернионов непрерывно; отображение x ↦ x, трактуемое как кватернион, непрерывно.

LaTeX

$$$\mathrm{Continuous}(\mathrm{coe} : \mathbb{R} \to \mathbb{H})$$$

Lean4

@[continuity]
theorem continuous_coe : Continuous (coe : ℝ → ℍ) :=
  continuous_algebraMap ℝ ℍ

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