English
The restriction map applied to x equals applying the original map to the function that uses x on P-parts and z elsewhere.
Русский
Применение ограничения домена к аргументу x эквивалентно применению исходной карты к функции, которая использует x на частях P и z вне их.
LaTeX
$$$ f.domDomRestrict P z x = f(\\lambda j, if P j then x(j) else z(j)) $$$
Lean4
theorem domDomRestrict_aux {ι} [DecidableEq ι] (P : ι → Prop) [DecidablePred P] {M₁ : ι → Type*}
[DecidableEq { a // P a }] (x : (i : { a // P a }) → M₁ i) (z : (i : { a // ¬P a }) → M₁ i) (i : { a : ι // P a })
(c : M₁ i) :
(fun j ↦ if h : P j then Function.update x i c ⟨j, h⟩ else z ⟨j, h⟩) =
Function.update (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) i c :=
by
ext j
by_cases h : j = i <;> grind [Function.update_self, Function.update_of_ne]
