orthogonalComplement_eq_orthogonalComplement

English

Kᗮ = Lᗮ implies K = L, when both have projections.

Русский

Kᗮ = Lᗮ тогда и только тогда K = L, если обе имеют ортогональные проекции.

LaTeX

$$$K^{\perp} = L^{\perp} \iff K = L$$$

Lean4

@[simp]
theorem orthogonalComplement_eq_orthogonalComplement {L : Submodule 𝕜 E} [K.HasOrthogonalProjection]
    [L.HasOrthogonalProjection] : Kᗮ = Lᗮ ↔ K = L :=
  ⟨fun h ↦ by simpa using congr(Submodule.orthogonal $(h)), fun h ↦ congr(Submodule.orthogonal $(h))⟩

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