logSpace — Mathlib

English

logSpace(K) is the real-valued function space on { w ∈ InfinitePlace(K) | w ≠ w0 }.

Русский

logSpace(K) — пространство вещественных значений на множестве { w ∈ InfinitePlace(K) | w ≠ w0 }.

LaTeX

$$$\mathrm{logSpace}(K) = \{ w: \mathrm{InfinitePlace}(K) \mid w \neq w_0 \} \to \mathbb{R}$$$

Lean4

/-- The `logSpace` is defined as `{w : InfinitePlace K // w ≠ w₀} → ℝ` where `w₀` is the
distinguished infinite place. -/
abbrev logSpace :=
  { w : InfinitePlace K // w ≠ w₀ } → ℝ

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