top_rpow_def — Mathlib

English

The top element’s real power is defined by a simple formula: (⊤)^y equals the indicated piecewise value depending on y.

Русский

Для верхнего элемента определение x^y задаётся через кусочно-определённую формулу в зависимости от y.

LaTeX

$$$(\\top)^{y} = \\begin{cases} \\top & 0

Lean4

theorem top_rpow_def (y : ℝ) : (⊤ : ℝ≥0∞) ^ y = if 0 < y then ⊤ else if y = 0 then 1 else 0 :=
  rfl

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