extend_def — Mathlib

English

For all i, Pi.map f (update g i a) equals update (Pi.map f g) i (f i a).

Русский

Для каждого i верно: Pi.map f (update g i a) = update (Pi.map f g) i (f i a).

LaTeX

$$$\mathrm{Pi.map}\ f\ (\mathrm{update}\ g\ i\ a) = \mathrm{update}\ (\mathrm{Pi.map}\ f\ g)\ i\ (f\ i\ a)$$$

Lean4

theorem extend_def (f : α → β) (g : α → γ) (e' : β → γ) (b : β) [Decidable (∃ a, f a = b)] :
    extend f g e' b = if h : ∃ a, f a = b then g (Classical.choose h) else e' b :=
  by
  unfold extend
  congr

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