all_balance'

Mathlib.Data.Ordmap.Invariants

URI: https://scilib.ai/kg/mathlib#Ordnode.all_balance'

← MathLib Explorer

English

All P on balance'(l, x, r) is equivalent to All P l ∧ P x ∧ All P r.

Русский

All P на balance'(l, x, r) эквивалентно All P l ∧ P x ∧ All P r.

LaTeX

$$All P (balance' l x r) \iff All P l ∧ P x ∧ All P r$$

Lean4

theorem all_balance' {P l x r} : @All α P (balance' l x r) ↔ All P l ∧ P x ∧ All P r := by rw [balance'];
  split_ifs <;> simp [all_node', all_rotateL, all_rotateR]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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