ext_iff — Mathlib

English

Two star projections are equal if and only if their ranges are equal.

Русский

Две звездные проекции равны тогда и только тогда, когда их диапазоны равны.

LaTeX

$$$$S = T \iff \operatorname{range}(S) = \operatorname{range}(T).$$$$

Lean4

/-- Star projection operators are equal iff their range are. -/
theorem ext_iff {S T : E →ₗ[𝕜] E} (hS : IsStarProjection S) (hT : IsStarProjection T) :
    S = T ↔ LinearMap.range S = LinearMap.range T :=
  by
  have := FiniteDimensional.complete 𝕜 E
  simpa using
    ContinuousLinearMap.IsStarProjection.ext_iff (S.isStarProjection_toContinuousLinearMap_iff.mpr hS)
      (T.isStarProjection_toContinuousLinearMap_iff.mpr hT)

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