rpow_eq_top_iff — Mathlib

English

x^y = ∞ iff (x=0 and y<0) or (x=∞ and y>0).

Русский

x^y = ∞ тогда и только тогда, когда (x=0 и y<0) или (x=∞ и y>0).

LaTeX

$$$x^y = \\infty \\iff (x=0 \\land y<0) \\lor (x=\\infty \\land y>0)$$$

Lean4

@[simp]
theorem rpow_eq_top_iff {x : ℝ≥0∞} {y : ℝ} : x ^ y = ⊤ ↔ x = 0 ∧ y < 0 ∨ x = ⊤ ∧ 0 < y := 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]

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