valid — Mathlib

English

Insertion with a general f preserves validity: if the type is total and LE is decidable, then insertWith f x t is valid whenever t is valid.

Русский

Вставка через insertWith сохраняет валидность: если тип полностью упорядочен и LE разрешима, то insertWith f x t валиден при валидности t.

LaTeX

$$$\\forall f,x,\\ hf:\\forall t,\\mathrm{Valid}(t)\\Rightarrow \\mathrm{Valid}(\\mathrm{insertWith} f x t)$$$

Lean4

theorem valid [IsTotal α (· ≤ ·)] [DecidableLE α] (f : α → α) (x : α) (hf : ∀ y, x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x) {t}
    (h : Valid t) : Valid (insertWith f x t) :=
  (insertWith.valid_aux _ _ hf h ⟨⟩ ⟨⟩).1

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