coe_prodEquivOfClosedCompl_symm — Mathlib

English

If p and q are subspaces of a normed space E with E = p ⊕ q and p, q closed, then the canonical product decompositions E ≅ p × q coming from the closed complement and from IsCompl coincide.

Русский

Пусть p и q — подпространства нормы пространства E такие, что E = p ⊕ q, и p, q замкнуты. Тогда канонические разложения E ≅ p × q, полученные из замкнутого дополнения и из IsCompl, совпадают.

LaTeX

$$$\big(p\text{.prodEquivOfClosedCompl } q h hp hq\big)^{-1} = \big(p\text{.prodEquivOfIsCompl } q h\big)^{-1}$$$

Lean4

@[simp]
theorem coe_prodEquivOfClosedCompl_symm (h : IsCompl p q) (hp : IsClosed (p : Set E)) (hq : IsClosed (q : Set E)) :
    ⇑(p.prodEquivOfClosedCompl q h hp hq).symm = (p.prodEquivOfIsCompl q h).symm :=
  rfl

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