div_nat_le_self_of_nonnneg

Mathlib.Algebra.Order.Field.Basic

URI: https://scilib.ai/kg/mathlib#div_nat_le_self_of_nonnneg

← MathLib Explorer

English

If a ≥ 0 and n ∈ N, then a / n ≤ a.

Русский

Если a ≥ 0 и n ∈ N, то a/n ≤ a.

LaTeX

$$$0 \le a \Rightarrow \forall n \in \mathbb{N}, \ \frac{a}{n} \le a$$$

Lean4

theorem div_nat_le_self_of_nonnneg (ha : 0 ≤ a) (n : ℕ) : a / n ≤ a :=
  if h : n = 0 then by simpa [h] using ha else div_le_self ha (n.one_le_cast_iff_ne_zero.mpr h)

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

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

Разделы

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

Аффилиация

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