ofIsCompl_eq — Mathlib

English

There is a natural linear equivalence between the pair of restricted maps (on p and q) and the whole space E → F when p and q are complementary.

Русский

Существует естественное линейное эквивалентное отображение между парой ограниченных отображений (на p и q) и всем пространством E → F, когда p и q комплементны.

LaTeX

$$$\text{Given } h:IsCompl(p,q),\; (φ,ψ): p→F × q→F,\; ((φ,ψ)\mapsto ofIsCompl h φ ψ): E→F.$$$

Lean4

theorem ofIsCompl_eq (h : IsCompl p q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} {χ : E →ₗ[R] F} (hφ : ∀ u, φ u = χ u)
    (hψ : ∀ u, ψ u = χ u) : ofIsCompl h φ ψ = χ := by
  ext x
  obtain ⟨_, _, rfl, _⟩ := existsUnique_add_of_isCompl h x
  simp [ofIsCompl, hφ, hψ]

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