orthogonal_orthogonal — Mathlib

English

For any subspace K with projection, Kᗮᗮ = K.

Русский

Для подппроступвающего K с проекцией Kᗮᗮ = K.

LaTeX

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

Lean4

/-- If `K` admits an orthogonal projection, then the orthogonal complement of its orthogonal
complement is itself. -/
@[simp]
theorem orthogonal_orthogonal [K.HasOrthogonalProjection] : Kᗮᗮ = K :=
  by
  ext v
  constructor
  · obtain ⟨y, hy, z, hz, rfl⟩ := K.exists_add_mem_mem_orthogonal v
    intro hv
    have hz' : z = 0 := by
      have hyz : ⟪z, y⟫ = 0 := by simp [hz y hy, inner_eq_zero_symm]
      simpa [inner_add_right, hyz] using hv z hz
    simp [hy, hz']
  · intro hv w hw
    rw [inner_eq_zero_symm]
    exact hw v hv

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