range_toContinuousMultilinearMap — Mathlib

English

The range of toContinuousMultilinearMap consists exactly of those maps that vanish whenever two coordinates coincide in some position.

Русский

Образ toContinuousMultilinearMap состоит из тех отображений, которые обращаются в нуль, когда два аргумента совпадают на каком-либо месте.

LaTeX

$$$ \\operatorname{range}(\\mathrm{toContinuousMultilinearMap}) = \\{ f : \\mathrm{ContinuousMultilinearMap} \\mid \\forall v,i,j,\\ v_i = v_j \\Rightarrow i \\neq j \\Rightarrow f(v)=0 \\}$$$

Lean4

theorem range_toContinuousMultilinearMap :
    Set.range (toContinuousMultilinearMap : M [⋀^ι]→L[R] N → ContinuousMultilinearMap R (fun _ : ι => M) N) =
      {f | ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → f v = 0} :=
  Set.ext fun f => ⟨fun ⟨g, hg⟩ => hg ▸ g.2, fun h => ⟨⟨f, h⟩, rfl⟩⟩

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