isClosed_range_toContinuousMultilinearMap

English

The alternatization of a continuous multilinear map f, when viewed as an alternating map via toAlternatingMap, equals the canonical alternating map built from f via MultilinearMap.alternatization.

Русский

Чередование отображения f, когда оно рассматривается как чередующее отображение через toAlternatingMap, совпадает с каноническим чередующим отображением, построенным из f через MultilinearMap.alternatization.

LaTeX

$$$$ (alternatization f).toAlternatingMap = MultilinearMap.alternatization f.toMultilinearMap. $$$$

Lean4

theorem isClosed_range_toContinuousMultilinearMap [ContinuousSMul 𝕜 E] [T2Space F] :
    IsClosed
      (Set.range (toContinuousMultilinearMap : (E [⋀^ι]→L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun _ : ι ↦ E) F)) :=
  by
  simp only [range_toContinuousMultilinearMap, setOf_forall]
  repeat refine isClosed_iInter fun _ ↦ ?_
  exact isClosed_singleton.preimage (continuous_eval_const _)

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