orthogonal_eq_bot_iff — Mathlib

English

K⊥ = ⊥ iff K = ⊤, given projections.

Русский

K⊥ = ⊥ тогда и только тогда K = ⊤ при наличии проекций.

LaTeX

$$$K^{\perp} = \{0\} \iff K = E$$$

Lean4

@[simp]
theorem orthogonal_eq_bot_iff [K.HasOrthogonalProjection] : Kᗮ = ⊥ ↔ K = ⊤ :=
  by
  refine ⟨?_, fun h => by rw [h, Submodule.top_orthogonal_eq_bot]⟩
  intro h
  have : K ⊔ Kᗮ = ⊤ := Submodule.sup_orthogonal_of_hasOrthogonalProjection
  rwa [h, sup_comm, bot_sup_eq] at this

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