piecewise_singleton — Mathlib

English

The piecewise construction on the singleton {x} equals the update of g at x by f(x).

Русский

Piecewise над множеством {x} равняется обновлению g в точке x значением f(x).

LaTeX

$$$\\text{piecewise}_{\\{x\\}}(f,g) = \\mathrm{update}_x g \\bigl(f(x)\\bigr)$$$

Lean4

theorem piecewise_singleton (x : α) [∀ y, Decidable (y ∈ ({ x } : Set α))] [DecidableEq α] (f g : α → β) :
    piecewise { x } f g = Function.update g x (f x) := by
  ext y
  by_cases hy : y = x
  · subst y
    simp
  · simp [hy]

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