ext_iff — Mathlib

English

Two symmetric projections S and T are equal if and only if their ranges coincide.

Русский

Две симметричные проекции S и T равны тогда и только тогда, когда их образы совпадают.

LaTeX

$$S IsSymmetricProjection, T IsSymmetricProjection ⇒ (S = T) ⇔ (range S = range T)$$

Lean4

/-- Symmetric projections are equal iff their range are. -/
theorem ext_iff {S T : E →ₗ[𝕜] E} (hS : S.IsSymmetricProjection) (hT : T.IsSymmetricProjection) :
    S = T ↔ LinearMap.range S = LinearMap.range T :=
  by
  refine ⟨fun h => h ▸ rfl, fun h => ?_⟩
  rw [hS.isIdempotentElem.ext_iff hT.isIdempotentElem, ←
    hT.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hT.isSymmetric, ←
    hS.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hS.isSymmetric]
  simp [h]

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