coe_continuous_linearProjOfClosedCompl'

English

Same as above, for the projection map equality version with a prime notation.

Русский

То же самое, но для равенства отображений проекции в форме с апострофом.

LaTeX

$$$p\text{.linearProjOfClosedCompl' } q h hp hq = p\text{.linearProjOfIsCompl } q h$$$

Lean4

@[simp]
theorem coe_continuous_linearProjOfClosedCompl' (h : IsCompl p q) (hp : IsClosed (p : Set E))
    (hq : IsClosed (q : Set E)) : ⇑(p.linearProjOfClosedCompl q h hp hq) = p.linearProjOfIsCompl q h :=
  rfl

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