English
A statement about completeness for a coherent family in the space of continuous alternating maps, extending the previous results.
Русский
Утверждение полноты для связной совокупности в пространстве непрерывных чередующих отображений, продолжение предыдущих результатов.
LaTeX
$$$$ \\text{completeSpace of ContinuousAlternatingMap under coherence} $$$$
Lean4
theorem completeSpace (h : IsCoherentWith {s : Set (ι → E) | IsVonNBounded 𝕜 s}) : CompleteSpace (E [⋀^ι]→L[𝕜] F) :=
by
wlog hF : T2Space F generalizing F
· rw [(isUniformInducing_postcomp (SeparationQuotient.mkCLM _ _)
SeparationQuotient.isUniformInducing_mk).completeSpace_congr]
· exact this inferInstance
· intro f
use (SeparationQuotient.outCLM _ _).compContinuousAlternatingMap f
ext
simp
have := ContinuousMultilinearMap.completeSpace (F := F) h
rw [completeSpace_iff_isComplete_range isUniformEmbedding_toContinuousMultilinearMap.isUniformInducing]
apply isClosed_range_toContinuousMultilinearMap.isComplete
