isCompl_of_proj — Mathlib

English

If f: E → p is such that f x = x for all x ∈ p, then p and ker f form a direct complement: IsCompl p (ker f).

Русский

Если отображение f: E → p удовлетворяет f x = x для всех x ∈ p, то p и ker f образуют прямое дополнение: IsCompl p (ker f).

LaTeX

$$$IsCompl\\ p\\ (\\ker f)$$$

Lean4

theorem isCompl_of_proj {f : E →ₗ[R] p} (hf : ∀ x : p, f x = x) : IsCompl p (ker f) :=
  by
  constructor
  · rw [disjoint_iff_inf_le]
    rintro x ⟨hpx, hfx⟩
    rw [SetLike.mem_coe, mem_ker, hf ⟨x, hpx⟩, mk_eq_zero] at hfx
    simp only [hfx, zero_mem]
  · rw [codisjoint_iff_le_sup]
    intro x _
    rw [mem_sup']
    refine ⟨f x, ⟨x - f x, ?_⟩, add_sub_cancel _ _⟩
    rw [mem_ker, LinearMap.map_sub, hf, sub_self]

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