insert_eq_insertWith — Mathlib

English

For any x and any t, insert' x t equals insertWith (constant x) x t; i.e., insert' behaves like insertWith of a constant function.

Русский

Для любого x и t, insert' x t равно insertWith (постоянная функция, возвращающая x) x t; insert' ведет себя как insertWith константы.

LaTeX

$$$\\forall x,\\ t:\\mathrm{Ordnode},\\ \\mathrm{insert'} x t = \\mathrm{insertWith}(\\lambda\\_.x)\\ x\\ t$$$

Lean4

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

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