le_orthogonal_iff_le_orthogonal — Mathlib

English

K0 ≤ K1ᗮ iff K1 ≤ K0ᗮ, given projections.

Русский

K0 ≤ K1ᗮ эквивалентно K1 ≤ K0ᗮ при наличии ортогональных проекций.

LaTeX

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

Lean4

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

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