top_orthogonal_eq_bot — Mathlib

English

The orthogonal of the whole subspace is the zero subspace: (⊤)⊥ = ⊥.

Русский

Ортогональное дополнение всего пространства равно нулевому подпространству: (⊤)⊥ = ⊥.

LaTeX

$$$(\top)^\perp = \bot$$$

Lean4

@[simp]
theorem top_orthogonal_eq_bot : (⊤ : Submodule 𝕜 E)ᗮ = ⊥ :=
  by
  ext x
  rw [mem_bot, mem_orthogonal]
  exact
    ⟨fun h => inner_self_eq_zero.mp (h x mem_top), by
      rintro rfl
      simp⟩

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