rpow_eq_zero_iff — Mathlib

English

For any y > 0, x^y = 0 if and only if x = 0.

Русский

Для любого y > 0, x^y = 0 эквивалентно x = 0.

LaTeX

$$$y>0 \\Rightarrow x^y = 0 \\iff x = 0$$$

Lean4

@[simp]
theorem rpow_eq_zero_iff {x : ℝ≥0∞} {y : ℝ} : x ^ y = 0 ↔ x = 0 ∧ 0 < y ∨ x = ⊤ ∧ y < 0 := by
  cases x with
  | top => rcases lt_trichotomy y 0 with (H | H | H) <;> simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]
  | coe x =>
    by_cases h : x = 0
    · rcases lt_trichotomy y 0 with (H | H | H) <;> simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]
    · simp [← coe_rpow_of_ne_zero h, h]

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