one_div_lt_one_div

Mathlib.Data.Nat.Cast.Order.Field

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

← MathLib Explorer

English

If n < m, then 1/(m+1) < 1/(n+1) in α.

Русский

Если n < m, то 1/(m+1) < 1/(n+1) в α.

LaTeX

$$$1 / ((m : α) + 1) < 1 / ((n : α) + 1) \quad (n < m)$$$

Lean4

theorem one_div_lt_one_div {n m : ℕ} (h : n < m) : 1 / ((m : α) + 1) < 1 / ((n : α) + 1) :=
  by
  refine one_div_lt_one_div_of_lt ?_ ?_
  · exact Nat.cast_add_one_pos _
  · simpa

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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