rotateL — Mathlib

English

If l and r are sized, then the rotated-left tree rotateL(l, x, r) is sized.

Русский

Если l и r имеют свойство ограниченности размера, то повернутое влево дерево rotateL(l, x, r) также ограничено по размеру.

LaTeX

$$(Sized(l)) ∧ (Sized(r)) ⟶ Sized(\mathrm{rotateL}(l, x, r))$$

Lean4

theorem rotateL {l x r} (hl : @Sized α l) (hr : Sized r) : Sized (rotateL l x r) :=
  by
  cases r; · exact hl.node' hr
  rw [Ordnode.rotateL_node]; split_ifs
  · exact hl.node3L hr.2.1 hr.2.2
  · exact hl.node4L hr.2.1 hr.2.2

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