sup_orthogonal_inf_of_hasOrthogonalProjection

English

If K1 ≤ K2 and K1 admits an orthogonal projection, then K1 ⊔ (K1⊥ ∩ K2) = K2.

Русский

Если K1 ≤ K2 и K1 допускает ортогональную проекцию, то K1 ⊔ (K1⊥ ∩ K2) = K2.

LaTeX

$$$K_1 \oplus (K_1^{\perp} \cap K_2) = K_2$$$

Lean4

/-- If `K₁` admits an orthogonal projection and is contained in `K₂`,
then `K₁` and `K₁ᗮ ⊓ K₂` span `K₂`. -/
theorem sup_orthogonal_inf_of_hasOrthogonalProjection {K₁ K₂ : Submodule 𝕜 E} (h : K₁ ≤ K₂)
    [K₁.HasOrthogonalProjection] : K₁ ⊔ K₁ᗮ ⊓ K₂ = K₂ := by
  ext x
  rw [Submodule.mem_sup]
  let v : K₁ := orthogonalProjection K₁ x
  have hvm : x - v ∈ K₁ᗮ := sub_starProjection_mem_orthogonal x
  constructor
  · rintro ⟨y, hy, z, hz, rfl⟩
    exact K₂.add_mem (h hy) hz.2
  · exact fun hx => ⟨v, v.prop, x - v, ⟨hvm, K₂.sub_mem hx (h v.prop)⟩, add_sub_cancel _ _⟩

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