right — Mathlib

English

If there exists a relation between sizes r1 and r2, then the sizes of the corresponding right subtrees in a node are likewise related by Raised.

Русский

Если существует отношение между размерностями r1 и r2, то размеры правых поддеревьев соответствующего узла также удовлетворяют Raised.

LaTeX

$$Raised(size(r1))(size(r2)) ∨ Raised(size(r2))(size(r2))$$

Lean4

theorem right {l x₁ x₂ r₁ r₂} (H : Raised (size r₁) (size r₂)) :
    Raised (size (@node' α l x₁ r₁)) (size (@node' α l x₂ r₂)) :=
  by
  rw [node', size_node, size_node]; generalize size r₂ = m at H ⊢
  rcases H with (rfl | rfl)
  · exact Or.inl rfl
  · exact Or.inr rfl

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