domDomRestrict_apply — Mathlib

English

Two domain-restricted multilinear maps coincide after a domain congruence σ if and only if the original maps coincide.

Русский

Две мультиленейные карты, ограниченные по домену, совпадают после конгруэнции доменов σ тогда, когда исходные карты совпадали.

LaTeX

$$$ f.domDomCongr σ = g.domDomCongr σ \\iff f = g $$$

Lean4

@[simp]
theorem domDomRestrict_apply (f : MultilinearMap R M₁ M₂) (P : ι → Prop) [DecidablePred P]
    (x : (i : { a // P a }) → M₁ i) (z : (i : { a // ¬P a }) → M₁ i) :
    f.domDomRestrict P z x = f (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) :=
  rfl

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