descFactorial_pos

Mathlib.Data.Nat.Factorial.Basic

URI: https://scilib.ai/kg/mathlib#Nat.descFactorial_pos

English

For all n,k ∈ ℕ, 0 < (n+1)^{\overline{k}}.

Русский

Для всех n,k ∈ ℕ: 0 < (n+1)^{\overline{k}}.

LaTeX

$$$$\forall n,k \in \mathbb{N}, 0 < (n+1)^{\overline{k}}$$$$

Lean4

@[simp]
theorem descFactorial_pos {n k : ℕ} : 0 < n.descFactorial k ↔ k ≤ n := by simp [Nat.pos_iff_ne_zero]

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

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

Разделы

Аффилиация

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