English
If a left-right balance condition holds, then the balanced dual configuration also yields a balanced split when sizes are transformed by duality.
Русский
Если выполняется условие баланса по левой и правой стороны, то сбалансированная двунаправленная конфигурация также дает сбалансированное разбиение после двойной дуализации размеров.
LaTeX
$$$\\text{balance\\_sz\\_dual}: \\text{If } H \\text{ holds, then } (\\exists l', Raised l'(\\mathrm{size}(dual r))\\land BalancedSz l'(\\mathrm{size}(dual l))) \\lor (\\exists r', Raised (\\mathrm{size}(dual l)) r' \\land BalancedSz (\\mathrm{size}(dual r)) r')$$$
Lean4
theorem balance_sz_dual {l r}
(H :
(∃ l', Raised (@size α l) l' ∧ BalancedSz l' (@size α r)) ∨ ∃ r', Raised r' (size r) ∧ BalancedSz (size l) r') :
(∃ l', Raised l' (size (dual r)) ∧ BalancedSz l' (size (dual l))) ∨
∃ r', Raised (size (dual l)) r' ∧ BalancedSz (size (dual r)) r' :=
by
rw [size_dual, size_dual]
exact
H.symm.imp (Exists.imp fun _ => And.imp_right BalancedSz.symm) (Exists.imp fun _ => And.imp_right BalancedSz.symm)
