valid — Mathlib

English

In a total preorder with decidable ≤, inserting into a valid tree using insert' preserves validity.

Русский

При полностью упорядоченном множестве с разрешимой предельностью ≤ вставка через insert' сохраняет валидность дерева.

LaTeX

$$$\\forall x,\\ t,\\ h:\\mathrm{Valid}(t)\\Rightarrow \\mathrm{Valid}(\\mathrm{insert'} x t)$$$

Lean4

theorem valid [IsTotal α (· ≤ ·)] [DecidableLE α] (x : α) {t} (h : Valid t) : Valid (Ordnode.insert x t) := by
  rw [insert_eq_insertWith]; exact insertWith.valid _ _ (fun _ _ => ⟨le_rfl, le_rfl⟩) h

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