size_le_size

Mathlib.Data.Nat.Size

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

English

If m ≤ n then size m ≤ size n.

Русский

Если m ≤ n, то size m ≤ size n.

LaTeX

$$$m \le n \Rightarrow \operatorname{size}(m) \le \operatorname{size}(n)$$$

Lean4

theorem size_le_size {m n : ℕ} (h : m ≤ n) : size m ≤ size n :=
  size_le.2 <| lt_of_le_of_lt h (lt_size_self _)

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

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

Разделы

Аффилиация

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