inv_pos_of_nat

Mathlib.Data.Nat.Cast.Order.Field

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

English

For any natural n, the inverse of (n + 1) in α is positive.

Русский

Для любого натурального n обратное (n + 1) в α положительное.

LaTeX

$$$0 < ((n : α) + 1)^{-1}$$$

Lean4

theorem inv_pos_of_nat {n : ℕ} : 0 < ((n : α) + 1)⁻¹ :=
  inv_pos.2 <| add_pos_of_nonneg_of_pos n.cast_nonneg zero_lt_one

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

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

Разделы

Аффилиация

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