powHalf — Mathlib

English

In Surreal numbers, powHalf(n) corresponds to the surreal number obtained from the pair (PGame.powHalf n, PGame.numeric_powHalf n).

Русский

В сюрреалах powHalf(n) соответствует сюрреальному числу, получаемому из пары (PGame.powHalf n, PGame.numeric_powHalf n).

LaTeX

$$powHalf(n) = \llbracket \langle PGame.powHalf(n), PGame.numeric\_powHalf(n) \rangle \rrbracket$$

Lean4

/-- Powers of the surreal number `half`. -/
def powHalf (n : ℕ) : Surreal :=
  ⟦⟨PGame.powHalf n, PGame.numeric_powHalf n⟩⟧

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