English
Given a predicate P on indices and a sampling z for the non-P indices, construct a multilinear map on the subtuple consisting of coordinates with P true by using the original map on mixed coordinates.
Русский
Для предиката P над индексами и выборки z для не-P координат, строим мультиленейную карту на подпоследовательность координат с P, используя исходную карту на смешанных координатах.
LaTeX
$$def domDomRestrict (f) (P) (z) : MultilinearMap R (fun (i : { a : ι // P a }) => M₁ i) M₂$$
Lean4
/-- The results of applying `domDomCongr` to two maps are equal if
and only if those maps are. -/
@[simp]
theorem domDomCongr_eq_iff (σ : ι₁ ≃ ι₂) (f g : MultilinearMap R (fun _ : ι₁ => M₂) M₃) :
f.domDomCongr σ = g.domDomCongr σ ↔ f = g :=
(domDomCongrEquiv σ : _ ≃+ MultilinearMap R (fun _ => M₂) M₃).apply_eq_iff_eq
