zero_rpow_def — Mathlib

English

For any real y, 0^y equals 0 if y>0, equals 1 if y=0, and equals infinity if y<0.

Русский

Для любого y: 0^y = 0, если y>0; 0^y = 1, если y=0; 0^y = бесконечность, если y<0.

LaTeX

$$$(0)^y = \\begin{cases}0 & y>0 \\\\ 1 & y=0 \\\\ \\infty & y<0\\end{cases}$$$

Lean4

theorem zero_rpow_def (y : ℝ) : (0 : ℝ≥0∞) ^ y = if 0 < y then 0 else if y = 0 then 1 else ⊤ :=
  by
  rcases lt_trichotomy (0 : ℝ) y with (H | rfl | H)
  · simp [H, zero_rpow_of_pos]
  · simp
  · simp [H, asymm H, ne_of_lt, zero_rpow_of_neg]

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