valid — Mathlib

English

If f is strictly monotone, then mapping f over a valid tree yields a valid tree.

Русский

Если f строго монотонна, отображение f над валидным деревом даёт валидное дерево.

LaTeX

$$$\\forall f:\\alpha\\to\\beta \\ (\\text{StrictMono } f)\\ {t},\\ h:\\mathrm{Valid}(t)\\Rightarrow \\mathrm{Valid}(\\mathrm{map}\\ f\\ t)$$$

Lean4

theorem valid {β} [Preorder β] {f : α → β} (f_strict_mono : StrictMono f) {t} (h : Valid t) : Valid (map f t) :=
  (Valid'.map_aux f_strict_mono h).1

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