mixedSpace — Mathlib

English

Let K be a field with signature (r1, r2). The mixed space is the product real space ℝ^{r1} × ℂ^{r2}, endowed with the standard Euclidean structure, hence a real Euclidean space.

Русский

Пусть K — поле с сигнатурой (r1, r2). Смешанное пространство равно ℝ^{r1} × ℂ^{r2}, на котором задана стандартная евклидова структура; это конечномерное евклидово пространство над ℝ.

LaTeX

$$$(\mathbb{R}^{r_1} \times \mathbb{C}^{r_2}, \langle \cdot, \cdot \rangle)$ является вещественным евклидовым пространством.$$

Lean4

/-- The mixed space `ℝ^r₁ × ℂ^r₂`, with `(r₁, r₂)` the signature of `K`, as an Euclidean space. -/
protected abbrev mixedSpace :=
  (WithLp 2
    ((EuclideanSpace ℝ { w : InfinitePlace K // IsReal w }) ×
      (EuclideanSpace ℂ { w : InfinitePlace K // IsComplex w })))

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