dec

Mathlib.Data.Ordmap.Invariants

URI: https://scilib.ai/kg/mathlib#Ordnode.BalancedSz.dec

English

The relation BalancedSz is decidable; for all l, r ∈ ℕ, BalancedSz(l, r) can be decided.

Русский

Отношение BalancedSz разрешимо; для любых l, r ∈ ℕ предикат BalancedSz(l, r) можно решить.

LaTeX

$$$$\forall l,r \in \mathbb{N},\; \operatorname{Decidable}(\operatorname{BalancedSz}(l,r)).$$$$

Lean4

instance dec : DecidableRel BalancedSz := fun _ _ => inferInstanceAs (Decidable (_ ∨ _))

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

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

Разделы

Аффилиация

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