balancedSz_zero

Mathlib.Data.Ordmap.Invariants

URI: https://scilib.ai/kg/mathlib#Ordnode.balancedSz_zero

English

For any l ∈ ℕ, BalancedSz(l, 0) holds if and only if l ≤ 1.

Русский

Для любого l ∈ ℕ BalancedSz(l, 0) верно тогда и только тогда, когда l ≤ 1.

LaTeX

$$$$\operatorname{BalancedSz}(l,0) \iff l \le 1.$$$$

Lean4

theorem balancedSz_zero {l : ℕ} : BalancedSz l 0 ↔ l ≤ 1 := by simp +contextual [BalancedSz]

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

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

Разделы

Аффилиация

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