English
If f is strictly monotone, mapping f over a valid tree preserves validity and preserves size.
Русский
Если f строго монотонна, отображение f над валидным деревом сохраняет валидность и размер остаётся неизменным.
LaTeX
$$$\\forall f:\\alpha\\to\\beta\\ (\\text{StrictMono } f)\\ ∀ t,a_1,a_2,\\ h:\\mathrm{Valid}' a_1 t a_2\\Rightarrow \\mathrm{Valid}'(\\mathrm{Option.map} f a_1)(\\mathrm{map} f t)(\\mathrm{Option.map} f a_2) \\land (\\mathrm{map} f t).size = t.size$$$
Lean4
theorem map_aux {β} [Preorder β] {f : α → β} (f_strict_mono : StrictMono f) {t a₁ a₂} (h : Valid' a₁ t a₂) :
Valid' (Option.map f a₁) (map f t) (Option.map f a₂) ∧ (map f t).size = t.size := by
induction t generalizing a₁ a₂ with
| nil =>
simp only [map, size_nil, and_true]; apply valid'_nil
cases a₁; · trivial
cases a₂; · trivial
simp only [Option.map, Bounded]
exact f_strict_mono h.ord
| node _ _ _ _ t_ih_l t_ih_r =>
have t_ih_l' := t_ih_l h.left
have t_ih_r' := t_ih_r h.right
clear t_ih_l t_ih_r
obtain ⟨t_l_valid, t_l_size⟩ := t_ih_l'
obtain ⟨t_r_valid, t_r_size⟩ := t_ih_r'
simp only [map, size_node, and_true]
constructor
· exact And.intro t_l_valid.ord t_r_valid.ord
· constructor
· rw [t_l_size, t_r_size]; exact h.sz.1
· constructor
· exact t_l_valid.sz
· exact t_r_valid.sz
· constructor
· rw [t_l_size, t_r_size]; exact h.bal.1
· constructor
· exact t_l_valid.bal
· exact t_r_valid.bal
