orthogonal_le_iff_orthogonal_le — Mathlib

English

K0⊥ ≤ K1⊥ iff K1 ≤ K0 in the presence of orthogonal projections.

Русский

При наличии ортогональных проекций K0⊥ ≤ K1⊥ тогда и только тогда K1 ≤ K0⊥.

LaTeX

$$$K_0^{\perp} \le K_1^{\perp} \iff K_1 \le K_0$$$

Lean4

theorem orthogonal_le_iff_orthogonal_le {K₀ K₁ : Submodule 𝕜 E} [K₀.HasOrthogonalProjection]
    [K₁.HasOrthogonalProjection] : K₀ᗮ ≤ K₁ ↔ K₁ᗮ ≤ K₀ := by rw [← orthogonal_le_orthogonal_iff, orthogonal_orthogonal]

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