size_eq_zero

Mathlib.Data.Nat.Size

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

English

For all n ∈ ℕ, size n = 0 iff n = 0.

Русский

Для всех n ∈ ℕ размер равен нулю тогда и только тогда, когда n = 0.

LaTeX

$$$\operatorname{size}(n) = 0 \iff n = 0$$$

Lean4

theorem size_eq_zero {n : ℕ} : size n = 0 ↔ n = 0 := by simpa [Nat.pos_iff_ne_zero, not_iff_not] using size_pos

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

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

Разделы

Аффилиация

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