all_node4L — Mathlib

English

All P on node4L(l, x, m, y, r) is equivalent to All P l ∧ P x ∧ All P m ∧ P y ∧ All P r.

Русский

All P на узле node4L(l, x, m, y, r) эквивалентно All P l ∧ P x ∧ All P m ∧ P y ∧ All P r.

LaTeX

$$@All P (node4L l x m y r) \iff All P l ∧ P x ∧ All P m ∧ P y ∧ All P r$$

Lean4

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

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