symm

Mathlib.Data.Ordmap.Invariants

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

English

If BalancedSz(l, r) holds, then BalancedSz(r, l) also holds.

Русский

Если BalancedSz(l, r) верно, то BalancedSz(r, l) также верно.

LaTeX

$$$$\operatorname{BalancedSz}(l,r) \rightarrow \operatorname{BalancedSz}(r,l).$$$$

Lean4

@[symm]
theorem symm {l r : ℕ} : BalancedSz l r → BalancedSz r l :=
  Or.imp (by rw [add_comm]; exact id) And.symm

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

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

Разделы

Аффилиация

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