right_le_pair

Mathlib.Data.Nat.Pairing

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

← MathLib Explorer

English

For any a,b, b ≤ pair(a,b).

Русский

Для любых a,b выполняется b ≤ pair(a,b).

LaTeX

$$$ \forall a,b \in \mathbb{N}, \; b \le \operatorname{pair}(a,b). $$$

Lean4

theorem right_le_pair (a b : ℕ) : b ≤ pair a b := by
  by_cases h : a < b
  · simpa [pair, h] using le_trans (le_mul_self _) (Nat.le_add_right _ _)
  · simp [pair, h]

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

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

Разделы

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

Аффилиация

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