prodEquivOfClosedCompl — Mathlib

English

If p and q are closed subspaces forming a closed complement, then p × q is continuously isomorphic to E.

Русский

Если p и q образуют закрытое дополнение и обе подподпространства замкнуты, то p × q непрерывно изоморфно E.

LaTeX

$$$$ (p \times q) \cong_L E.$$$$

Lean4

/-- If `q` is a closed complement of a closed subspace `p`, then `p × q` is continuously
isomorphic to `E`. -/
def prodEquivOfClosedCompl (h : IsCompl p q) (hp : IsClosed (p : Set E)) (hq : IsClosed (q : Set E)) :
    (p × q) ≃L[𝕜] E := by
  haveI := hp.completeSpace_coe; haveI := hq.completeSpace_coe
  refine (p.prodEquivOfIsCompl q h).toContinuousLinearEquivOfContinuous ?_
  exact (p.subtypeL.coprod q.subtypeL).continuous

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