eq_zero_rpow_iff

Mathlib.Analysis.SpecialFunctions.Pow.Real

URI: https://scilib.ai/kg/mathlib#Real.eq_zero_rpow_iff

English

For any x,a ∈ ℝ, a = 0^x iff (x ≠ 0 ∧ a = 0) ∨ (x = 0 ∧ a = 1).

Русский

Для любых x,a ∈ ℝ, a = 0^x эквивалентно (x ≠ 0 и a = 0) или (x = 0 и a = 1).

LaTeX

$$$\\forall x,a \\in \\mathbb{R}, a = 0^x \\iff \\; (x \\neq 0 \\land a = 0) \\lor \\ (x = 0 \\land a = 1)$$$

Lean4

theorem eq_zero_rpow_iff {x : ℝ} {a : ℝ} : a = 0 ^ x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 := by
  rw [← zero_rpow_eq_iff, eq_comm]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru