insert'_eq_insertWith — Mathlib

English

For all α with preorder and decidable ≤, and all x, insert' x t equals insertWith id x t.

Русский

Для всех α с порядком и разрешимой ≤, и для всех x, insert' x t равно insertWith id x t.

LaTeX

$$$\\forall x,\\ t,\\ \\mathrm{insert'} x t = \\mathrm{insertWith}(\\mathrm{id}) x t$$$

Lean4

theorem insert'_eq_insertWith [DecidableLE α] (x : α) : ∀ t, insert' x t = insertWith id x t
  | nil => rfl
  | node _ l y r => by unfold insert' insertWith; cases cmpLE x y <;> simp [insert'_eq_insertWith]

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