English
Under monotone directed U, starProjection tendsto to closure of iSup of U.
Русский
При монотонной направленности U проекция-звезда сходится к замыканию iSup(U).
LaTeX
$$$\mathrm{starProjection}_{\bigvee_i U_i} \to \mathrm{starProjection}_{\bigcup_i U_i}$$$
Lean4
/-- Given a monotone family `U` of complete submodules of `E` with dense span supremum,
and a fixed `x : E`, the orthogonal projection of `x` on `U i` tends to `x` along `at_top`. -/
theorem starProjection_tendsto_self {ι : Type*} [Preorder ι] (U : ι → Submodule 𝕜 E)
[∀ t, (U t).HasOrthogonalProjection] (hU : Monotone U) (x : E) (hU' : ⊤ ≤ (⨆ t, U t).topologicalClosure) :
Filter.Tendsto (fun t => (U t).starProjection x) atTop (𝓝 x) :=
by
have : (⨆ i, U i).topologicalClosure.HasOrthogonalProjection :=
by
rw [top_unique hU']
infer_instance
convert starProjection_tendsto_closure_iSup U hU x
rw [eq_comm, starProjection_eq_self_iff, top_unique hU']
trivial
