English
For any number field K, the mixed space is the Cartesian product of real-valued functions on real places and complex-valued functions on complex places. Concretely, it is the product ( { w : InfinitePlace K | IsReal w } → ℝ ) × ( { w : InfinitePlace K | IsComplex w } → ℂ ).
Русский
Для любой числовой поля K смешанное пространство есть произведение: набор функций из действительных мест в ℝ и набор функций из комплексных мест в ℂ; то есть ({ w : InfinitePlace K | IsReal w } → ℝ) × ({ w : InfinitePlace K | IsComplex w } → ℂ).
LaTeX
$$$\mathrm{mixedSpace}(K) = \left(\{ w : \mathrm{InfinitePlace}(K) \mid \mathrm{IsReal}(w) \} \to \mathbb{R}\right) \times \left(\{ w : \mathrm{InfinitePlace}(K) \mid \mathrm{IsComplex}(w) \} \to \mathbb{C}\right).$$$
Lean4
/-- The mixed space `ℝ^r₁ × ℂ^r₂` with `(r₁, r₂)` the signature of `K`. -/
abbrev mixedSpace :=
({ w : InfinitePlace K // IsReal w } → ℝ) × ({ w : InfinitePlace K // IsComplex w } → ℂ)
