left_le_pair

Mathlib.Data.Nat.Pairing

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

English

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

Русский

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

LaTeX

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

Lean4

theorem left_le_pair (a b : ℕ) : a ≤ pair a b := by simpa using unpair_left_le (pair a b)

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

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

Разделы

Аффилиация

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