one_div_le_one_div

Mathlib.Data.Nat.Cast.Order.Field

URI: https://scilib.ai/kg/mathlib#Nat.one_div_le_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) \le 1 / ((n : α) + 1) \quad (n \le m)$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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