isNat_rpow_pos

Mathlib.Analysis.SpecialFunctions.Pow.Real

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.NormNum.isNat_rpow_pos

English

If b is a natural nb and a^nb is a natural ne, then a^b is a natural ne.

Русский

Если b — натуральное nb и a^nb — натуральное ne, то a^b — натуральное ne.

LaTeX

$$IsNat b nb → IsNat (a ^ nb) ne → IsNat (a ^ b) ne$$

Lean4

theorem isNat_rpow_pos {a b : ℝ} {nb ne : ℕ} (pb : IsNat b nb) (pe' : IsNat (a ^ nb) ne) : IsNat (a ^ b) ne := by
  rwa [pb.out, rpow_natCast]

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

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

Разделы

Аффилиация

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