rotateR — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem rotateR {l x r} (hl : @Sized α l) (hr : Sized r) : Sized (rotateR l x r) :=
  Sized.dual_iff.1 <| by rw [dual_rotateR]; exact hr.dual.rotateL hl.dual

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