linearProjOfIsCompl_of_proj — Mathlib

English

The above linear equivalence is canonical and respects the projections to F and G.

Русский

Вышеупомянутое линейное эквивалентное отображение канонично и сохраняет проекции.

LaTeX

$$$f\equivProdOfSurjectiveOfIsCompl\ g\; hf\ hg\ hfg : E \simeq F\times G$$$

Lean4

@[simp]
theorem linearProjOfIsCompl_of_proj (f : E →ₗ[R] p) (hf : ∀ x : p, f x = x) :
    p.linearProjOfIsCompl (ker f) (isCompl_of_proj hf) = f :=
  by
  ext x
  have : x ∈ p ⊔ (ker f) := by simp only [(isCompl_of_proj hf).sup_eq_top, mem_top]
  rcases mem_sup'.1 this with ⟨x, y, rfl⟩
  simp [hf]

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