English
For l, x, r with Balanced l and Balanced r and the size constraints sl, sr and hypothesis H, All P on balanceR(l, x, r) is equivalent to All P on l, P on x, and All P on r.
Русский
Для l, x, r с сбалансированными l и r и размерными ограничениями sl, sr и гипотезой H, All P на balanceR(l, x, r) эквивалентно All P на l, P на x и All P на r.
LaTeX
$$$\forall P\ l\ x\ r,\ hl:\ Balanced\ l\ ∧ hr:\ Balanced\ r\ ∧ sl:\ Sized\ l\ ∧ sr:\ Sized\ r\ ∧ H,\ All\ P\ (balanceR\ l\ x\ r) \iff All\ P\ l \land P\ x \land All\ P\ r$$$
Lean4
theorem all_balanceR {P l x r} (hl : Balanced l) (hr : Balanced r) (sl : Sized l) (sr : Sized r)
(H : (∃ l', Raised (size l) l' ∧ BalancedSz l' (size r)) ∨ ∃ r', Raised r' (size r) ∧ BalancedSz (size l) r') :
All P (@balanceR α l x r) ↔ All P l ∧ P x ∧ All P r := by rw [balanceR_eq_balance' hl hr sl sr H, all_balance']
