isOrtho_top_right — Mathlib

English

A subspace U is orthogonal to the top subspace if and only if the subspace is zero.

Русский

Подмодуль U ортогонален верхнему подпространству тогда и только тогда, когда U = ⊥.

LaTeX

$$$\top \perp V \iff V = \bot$$$

Lean4

@[simp]
theorem isOrtho_top_right {U : Submodule 𝕜 E} : U ⟂ ⊤ ↔ U = ⊥ :=
  ⟨fun h => eq_bot_iff.mpr fun _x hx => inner_self_eq_zero.mp (h hx _ mem_top), fun h => h.symm ▸ isOrtho_bot_left⟩

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