all_rotateL

Mathlib.Data.Ordmap.Invariants

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$All P (rotateL l x r) \iff All P l ∧ P x ∧ All P r$$

Lean4

theorem all_rotateL {P l x r} : @All α P (rotateL l x r) ↔ All P l ∧ P x ∧ All P r := by
  cases r <;> simp [rotateL, all_node']; split_ifs <;> simp [all_node3L, all_node4L, All]

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

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

Разделы

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

Аффилиация

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