doubleFactorial_pos

Mathlib.Data.Nat.Factorial.DoubleFactorial

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

English

For every natural n, the double factorial n‼ is positive.

Русский

Для каждого натурального n двойной факториал n‼ положителен.

LaTeX

$$$ 0 < n‼ \quad \text{для всех } n \in \mathbb{N} $$$

Lean4

theorem doubleFactorial_pos : ∀ n, 0 < n‼
  | 0 | 1 => zero_lt_one
  | _n + 2 => mul_pos (succ_pos _) (doubleFactorial_pos _)

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

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

Разделы

Аффилиация

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