all_node4R — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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